[isabelle-dev] Infinite loops with output
abouzy at mpi-inf.mpg.de
Thu May 28 16:01:32 CEST 2015
> 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 ?
More information about the isabelle-dev