>   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.

>   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.

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

ProofGeneral-devel mailing list

Reply via email to