Finally, here is another way how isabelle-release/5adc68deb322 (i.e. after your first patch) appears to have proven a non-theorem. Load the following and just wait a moment until the tactic interrupts due to stack-overflow. The theorem's status gets failed, but this is not displayed in isabelle/jEdit, nor is there an error on the tactic-block.
I think that is a clear indication that the status failed can happen (stack-overflow, out-of-memory, what-so-ever), and should be displayed in isabelle/jEdit! ML {* fun stack_overflow a = a + 1 + stack_overflow a *} lemma f:False by (tactic {* let val _ = stack_overflow 0 in all_tac end*}) ML_val {* Thm.peek_status @{thm f} *} -- Peter On Do, 2013-11-21 at 13:11 +0100, Makarius wrote: > On Thu, 21 Nov 2013, Peter Lammich wrote: > > > On my machine, there is also a second way to run into this Problem: Just > > load a theory with a diverging command, and wait long enough > > (nondeterministically, between tens of seconds and several minutes). The > > command appears to finish, and the theorem's status is failed. > > I would guess that it is just another way to get edits applied eventually. > There are many timers in Isabelle/jEdit and the underlying Isabelle/Scala > infrastructure, e.g. for garbage collection of unused document versions. > > This is a highly interactive computer-game. The first time in the history > of "ITP" that interaction really happens. > > > > In an earlier message on this thread, you have posted a patch. However, > > I cannot apply this patch to the development repository, nor does the > > revision "db3d3d99c69d", which your patch refers to, exist. > > This mail thread is about the release: > https://bitbucket.org/isabelle_project/isabelle-release > > > Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev