Re: [PG-devel] Re: auto coppile hangs emacs

2011-05-06 Thread Hendrik Tews
David Aspinall writes: > Yes, but this will not be easy. The problem is the > following: I temporarily have to stop the proof-shell main > loop if the next item in proof-action-list is a Require and > if the corresponding compile job has not been finished. > > Simply calling ac

Re: [PG-devel] Re: auto coppile hangs emacs

2011-05-06 Thread David Aspinall
> Yes, but this will not be easy. The problem is the following: I > temporarily have to stop the proof-shell main loop if the next > item in proof-action-list is a Require and if the corresponding > compile job has not been finished. > > Simply calling accept-process-output inside proof-shell-exec

[PG-devel] Re: auto coppile hangs emacs

2011-05-06 Thread Hendrik Tews
Pierre Courtieu writes: > Emacs is locked because I avoided all synchronization trouble and > call coqdep and coqc synchronously. All this happens before the > asserted items are put into proof-action-list. > > This is not optimal, but for a first version it is hopefully ok.

[PG-devel] Re: auto coppile hangs emacs

2011-05-05 Thread Hendrik Tews
Hi, Pierre Courtieu writes: Is there a reason why emacs completely hangs when auto compilation is working? You mean emacs is locked until compilation is finished and all asserted items are in the queue region? Or do you mean something else? Emacs is locked because I avoided all synchr