Coq menu entries

[Hendrik Tews]

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?

It might be good to have "Electric Terminator" in the main Coq
menu but the other two could go into Settings menu IMHO.

[I understand that "Toggle 3 Windows Mode" cannot be inside
Settings, as defpacustom cannot handle radio button style submenus.]

Bye,

Hendrik

[Pierre Courtieu]

Post by Hendrik Tews
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.

Post by Hendrik Tews
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.

Post by Hendrik Tews
[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

[Hendrik Tews]

Pierre Courtieu <Pierre.Courtieu-***@public.gmane.org> 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.

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

[David Aspinall]

Post by Pierre Courtieu
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.

I agree, please go ahead Pierre.

Post by Pierre Courtieu
By the way is there a "emacs gui recommendations somewhere?"
I don't know any.

Me neither. There are recommendations about Emacs conventions scattered through the Lisp reference manuals and apart from that I try to follow what Emacs itself does and the standard applications it ships with.

- D.

[Pierre Courtieu]

Post by Pierre Courtieu
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.

Post by Pierre Courtieu
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
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel