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. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
