[isabelle-dev] Infinite loops with output

[Makarius]

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.


 	Makarius