OK, that makes sense to me. P.
2016-05-12 19:25 GMT+02:00 Paul A. Steckler <st...@stecksoft.com>: > On Thu, May 12, 2016 at 6:28 PM, Pierre Courtieu > <pierre.court...@cnam.fr> wrote: >> This is already the case AFAIK, in pg the queue is processed one >> element at a time (waiting for a prompt between each), so in fact >> there is a process that reads the queue and process it. No? > > In generic/proof-shell.el, there is procedure labeled "MAIN LOOP" that > I believe pulls items off the queue. > The procedures that add items to the queue are in the same file. > > All I'm suggesting is that the procedures that add items be moved out > of this file, and the queue itself, so that my server code as well as > the proof shell code can use the queue. > >> More generally can you take a few minutes explaining exactly where you >> want to go. The thing that I don't get in your approach is the >> following: >> >> If I understood well you still want to have a "locked region" as pg >> has currently, right? Then I don't understand why the current >> mechanism should change, especially if you manage to get a >> pseudoprompt after each command. > > The basic mechanism of queue handling won't change, just the code > organization. It's an issue of software engineering, rather than an > algorithmic issue. > > -- Paul _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
