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
