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
