[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