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
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 18:
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
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 among Coq users?
>
> --
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
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
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgener
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