[isabelle] Interrupt Isabelle with signal



Hi all,

I'm working on a program that starts Isabelle and communicates with the
Isabelle process (in Isar interaction mode) using its standard output and
input stream. Now I'd like to be able to cancel commands I've sent to
Isabelle (e.g. because their execution doesn't terminate). The
ProofGeneral seems to have this capability and uses
comint-interrupt-subjob in the proof-interrupt-process function. But when
I try to send a SIGINT signal to the isabelle-process, it doesn't have any
impact, however sending SIGINT to the poly process that isabelle starts
("poly-driver") manually, causes Isabelle to cancel the execution of the
current command (which is what I'm trying to do from within my program).
This is a problem, since I do not have a chance to get the process ID of
this poly-driver process that Isabelle spawns and therefore cannot send
signals to it (I do have Isabelle's PID, of cause). In the Isabelle System
Manual, I couldn't find out if there is a way to send signals to the
Isabelle process directly, neither how the ProofGeneral deals with this
problem.

-- Florian









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.