[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.


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