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 be
some way to extend the queue, independent of the proof shell (and
server), then some way to process the queue that  involves the proof
shell or server.

Does that make sense?

-- Paul
ProofGeneral-devel mailing list

Reply via email to