As I'm developing a separate server mode for PG, I'm noticing a tight
coupling between the queue of items for processing and proof shells,
which seems undesirable.
To wit, the procedures `proof-extend-queue` and `proof-add-to-queue`
are both found in generic/proof-shell.el. Probably there should b
2016-05-12 15:44 GMT+02:00 Paul A. Steckler :
> As I'm developing a separate server mode for PG, I'm noticing a tight
> coupling between the queue of items for processing and proof shells,
> which seems undesirable.
In PG these are in bijection indeed, except for queries that can be
sent to the pr
On Thu, May 12, 2016 at 6:28 PM, Pierre Courtieu
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 procedur
OK, that makes sense to me.
P.
2016-05-12 19:25 GMT+02:00 Paul A. Steckler :
> On Thu, May 12, 2016 at 6:28 PM, Pierre Courtieu
> 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 t