[isabelle-dev] Infinite loops with output

Makarius makarius at sketis.net
Thu May 28 15:38:57 CEST 2015

On Thu, 28 May 2015, Aymeric Bouzy wrote:

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

Using Isabelle/ML or SML inside Isabelle is a regular isabelle-users 
activity, so this is off-topic on this mailing list.

> The problem is that Isabelle/jEdit freezes as soon as an infinite output 
> is printed, as proven by the included file.

If you use "tracing" instead of "writeln" the front-end gets a chance to 
survive this massive DNS attack.

There is some kind of dialog at the bottom of the output window.


More information about the isabelle-dev mailing list