[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

[PG-devel] Proof tree code

2016-05-12 Thread Paul A. Steckler
The code in generic/proof-tree appears to rely on proof shell modes. Is the `prooftree' tool in common use among Coq users? -- Paul ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk

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

Re: [PG-devel] Proof tree code

2016-05-12 Thread Pierre Courtieu
I don't know. It is a nice peace of code. Maybe we can ask Hendrik to port it once you have something working. P. 2016-05-12 18:22 GMT+02:00 Paul A. Steckler : > The code in generic/proof-tree appears to rely on proof shell modes. > > Is the `prooftree' tool in common use

Re: [PG-devel] Proof tree code

2016-05-12 Thread Clément Pit--Claudel
I think this would be the right strategy; Hendrik has been pretty good at keeping it up to until this point :) On 2016-05-12 12:33, Pierre Courtieu wrote: > I don't know. It is a nice peace of code. Maybe we can ask Hendrik to > port it once you have something working. > > P. > > 2016-05-12

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
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