2012/11/14 Hendrik Tews <t...@os.inf.tu-dresden.de>: > Pierre Courtieu <pierre.court...@cnam.fr> writes: > > Since double hit terminator is more or less an alternative to electric > terminator, I have put them side by side in coq menu, to see if people > > OK, I thought "double hit" would modify the behavior of electric > terminator.
It does: it disables electric terminator. Both options are mutually exclusive (first time I used advicing function by the way). P. > like it, but I did not make it geenric yet. Maybe one entry for both > settings with a 3-value setting would be better? > > >From the user perspective this would certainly be better. But if > the implementation is not trivial, we can also keep the two > settings. > > Actually tooltips are so useless and annoying (flickering) in coq mode > that I wanted the disabling option to be as immediate as possible. It > would probably be better to disable it by default and put the option > in the settings menu. > > Fine with me. > > By the way is there a "emacs gui recommendations somewhere?" > > I don't know any. BTW, I just wanted to ask. I don't really have > a strong opinion where those items should go. > > Bye, > > Hendrik > _______________________________________________ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
