[isabelle-dev] Isabelle2009 fails to handle interrupts
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.
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!
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
More information about the isabelle-dev