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.
   It is indeed ok but it may be worth allowing the user to be able to
   edit unlocked region during this time. This can be a feature of second
   version :)
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-loop
does not help, because emacs does not process keyboard input
during waiting inside accept-process-output. 

There seems to be no way around aborting proof-shell-exec-loop in
the middle and restarting it when the compile job has finished.


ProofGeneral-devel mailing list

Reply via email to