>   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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to