2012/11/13 Hendrik Tews <t...@os.inf.tu-dresden.de>: > Hi, > > I just noticed that there are a view boolean settings in the Coq > menu which are not done via defpacustom and which are therefore > not in the Settings submenu. Is there a reason, why "Toggle > tooltips", "Electric Terminator" and "Double Hit Electric > Terminator" are not in the Settings submenu?
They are, except double hit terminator which is experimental. They are in pg/quick options because they are generic settings. > It might be good to have "Electric Terminator" in the main Coq > menu but the other two could go into Settings menu IMHO. 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 like it, but I did not make it geenric yet. Maybe one entry for both settings with a 3-value setting would be better? This is still experimental (in particular I need to rework it because it has some flaws). 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. > [I understand that "Toggle 3 Windows Mode" cannot be inside > Settings, as defpacustom cannot handle radio button style submenus.] Until now I have been putting things in the main coq menu when I wanted to advertise the corresponding feature (no matter if it is a setting or a command). For instance I believe three windows mode is now very much used and I am not sure people would use it so much if it had been in the settings menu. By the way is there a "emacs gui recommendations somewhere?" Best Pierre _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
