[isabelle-dev] Infinite loops with output

Aymeric Bouzy abouzy at mpi-inf.mpg.de
Thu May 28 15:28:26 CEST 2015


I'm doing some development in SML for Isabelle, and sometimes I accidentally write an infinite loop. To try to determine where the infinite loops comes from, I often print some output, as this is the recommanded way to debug SML code I believe.

The problem is that Isabelle/jEdit freezes as soon as an infinite output is printed, as proven by the included file.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Development.thy
Type: application/octet-stream
Size: 112 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150528/2a430a84/attachment.obj>
-------------- next part --------------

I haven't found a way yet to interrupt the execution of the file, so does this feature exist? and if no, could it be considered adding it?


Aymeric Bouzy

More information about the isabelle-dev mailing list