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