Re: [isabelle] Interrupt Isabelle with signal



On Wed, 11 Jul 2007, Florian Funke wrote:

> 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

Peeking at comint.el reveals that emacs signals the whole process group of 
the controlling pty here.  I've managed to imitate this behaviour in the 
shell using kill with negated PID like this:

  kill -INT -- -4711

Also note that the Isabelle/Isar toplevel ignores any INT signals unless 
it actually runs a command.  To test kills more easily you may use the raw 
ML toplevel, which reports something like ``Compilation interrupted''.


	Makarius





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