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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
