# HG changeset patch
# User wenzelm
# Date 1357844018 -3600
# Node ID 1702ed63c2db6632f3ebb851a2a3e04345a122ec
# Parent  c065f3d1419779c58a38b58650872723ce0e7c17
more general prover termination dialog, which might indicate undetected failure or just ML "exit 0";

diff -r c065f3d14197 -r 1702ed63c2db src/Tools/jEdit/src/plugin.scala
--- 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()))
               }