[isabelle-dev] Infinite loops with output

[Aymeric Bouzy]

> On 28 May 2015, at 15:38, Makarius <makarius at sketis.net> wrote:
> 
> Using Isabelle/ML or SML inside Isabelle is a regular isabelle-users activity, so this is off-topic on this mailing list.

Sorry about that, you are right.
> 
> 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.

This was exactly what I was looking for ! Thanks a lot.

Maybe it could be considered mentioning it in The Isabelle Cookbook in section 2.2 ?

Aymeric