[isabelle-dev] Infinite loops with output
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