Re: [PG-devel] Coq menu entries

2012-11-14 Thread David Aspinall
> 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

Re: [PG-devel] first version of parallel background compilation for Coq

2012-11-14 Thread Hendrik Tews
David Aspinall writes: > I just committed the first version of parallel background > compilation for Coq. It sounds very useful! Are there some Coq users who are testing for you? Not that I know. H. ___ ProofGeneral-devel mailing list Proo

Re: [PG-devel] Coq menu entries

2012-11-14 Thread Hendrik Tews
Pierre Courtieu 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

Re: [PG-devel] proof-shell-pre-interrupt-hook ?

2012-11-14 Thread David Aspinall
> I just came across proof-shell-pre-interrupt-hook. I can't find > any location where this hook is run. Am I missing something? Likely obsolete but let me check some old versions: http://proofgeneral.inf.ed.ac.uk/trac/ticket/457 -- The University of Edinburgh is a charitable body, registered

Re: [PG-devel] first version of parallel background compilation for Coq

2012-11-14 Thread David Aspinall
> I just committed the first version of parallel background > compilation for Coq. It sounds very useful! Are there some Coq users who are testing for you? - David -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. __