OK, that makes sense to me.

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

Reply via email to