more general prover termination dialog, which might indicate undetected failure or just ML "exit 0";
--- a/src/Tools/jEdit/src/plugin.scala Thu Jan 10 19:07:44 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Jan 10 19:53:38 2013 +0100
@@ -189,9 +189,9 @@
react {
case phase: Session.Phase =>
phase match {
- case Session.Failed =>
+ case Session.Inactive | Session.Failed =>
Swing_Thread.later {
- Library.error_dialog(jEdit.getActiveView, "Prover process failure",
+ Library.error_dialog(jEdit.getActiveView, "Prover process terminated",
"Isabelle Syslog", Library.scrollable_text(PIDE.session.current_syslog()))
}