David Aspinall <david.aspin...@ed.ac.uk> 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 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. Yes, I actually meant that the compilation is running in separate asynchronous subprocesses. However, I thought that all asserted commands are put into proof-action-list before proof-assert-until-point completes. Require commands are marked as unfinished when they are inserted into proof-action-list. When the asynchronous compilation process for some required library is finished the corresponding Require command is marked as finished. When proof-shell-exec-loop sees an unfinished Require command it suspends itself without inserting it into the proof shell. 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. You seem to suggest to keep unfinished Require commands (and all what follows such a command) in a separate list and add them only to proof-action-list when the compilation process is finished. This seems simpler. However, it would be nice, when still unfinished Require commands are colored pink as belonging to the queue region. Where is this pink coloring happening? I searched the subroutines of proof-assert-until-point, but did not find the function that is responsible for the pink color. 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). Fine with me. I would suggest that we deal with the following issues before releasing: - fix broken pg cache (http://proofgeneral.inf.ed.ac.uk/trac/ticket/395) - fix defpacustom customization groups (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000115.html) - decide on completion-ignored-extensions (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000122.html) Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
