Re: [PG-devel] Coupling of items queue and proof shell

2016-05-12 Thread Pierre Courtieu
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

Re: [PG-devel] Coupling of items queue and proof shell

2016-05-12 Thread 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 that reads the queue and process it. No? In

Re: [PG-devel] Coupling of items queue and proof shell

2016-05-12 Thread Pierre Courtieu
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

[PG-devel] Coupling of items queue and proof shell

2016-05-12 Thread 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. To wit, the procedures `proof-extend-queue` and `proof-add-to-queue` are both found in generic/proof-shell.el. Probably there should