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

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?"

ProofGeneral-devel mailing list

Reply via email to