[isabelle-dev] Isabelle2009 fails to handle interrupts
David Aspinall
David.Aspinall at ed.ac.uk
Mon Aug 17 18:57:40 CEST 2009
I don't believe this is PG's fault. I can reproduce problems in tty
mode. With the previous version, you sent C-c C-c and it reliably
interrupted and printed "*** Interrupted". With Isabelle2009 interrupts
may get ignored or go unreported and output and the following prompt may
or may not appear.
http://proofgeneral.inf.ed.ac.uk/trac/ticket/179
I've added some workaround but it's not easy to tell between a busy
prover and one that's been interrupted and stopped sending output but is
too secretive to tell you about it!
- David
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
More information about the isabelle-dev
mailing list