[isabelle-dev] Infinite loops with output

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


Hello,

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?

Thanks,

Aymeric Bouzy


More information about the isabelle-dev mailing list