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

No, I don't think you want to insert a wait inside proof-shell-exec-loop -- 
this is called from the process filter function for the prover just to handle 
the last prover output.

I guess the way to do things is to trigger the compilation in *another* 
asynchronous subprocess (I think you call coqc synchronously at the moment?) 
and use a filter function or process sentinel to handle the compile output.  
This would allow control to return to the ordinary top level.  Then the filter 
function goes back to call the insertion function which sends Require to the 
prover, if the compile succeeded.  The exec loop picks up automatically again.

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

No, but that seems OK: this should just appear as if the prover is busy, so 
preventing undo, etc.  (You may need to take extra action on interrupts)

Anyway, I agree this improvement is probably for v2.  We should try to release 
PG 4.1 in the next couple of weeks (at last).

 - D.

ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to