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

   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

- decide on completion-ignored-extensions


ProofGeneral-devel mailing list

Reply via email to