On Thu, 21 Nov 2013, Peter Lammich wrote:
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!
After diagnosing the problem, I did put a note on my TODO list to make the
status reports more defensive, to allow system disintegration on the ML
side. E.g. the current order of status messages assumes that some later
bits of ML code have a chance to run.
This is just the normal process of continuous convergence of the system
towards an increasingly better state, which is ongoing for some decades
already. (An attempt to "fix" it now will inevitably break other things.)
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}
*}
The question here is if it is of practical relevance or just a synthetic
example. You could also raise Exn.Interrupt here directly.
The principle that Proof General and Isabelle/jEdit as interactive
front-ends are not required to be fully authentic still applies -- until
there is just one uniform document model for batch and interactive mode,
and no TTY nor Proof General anymore.
If a breakdown happens as easily as editing the text, it is a problem.
If it is merely a conceptual demonstration of breakability, if is not.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
