# HG changeset patch
# User wenzelm
# Date 1489403051 -3600
# Node ID ff8c3c29a9244bec45bbde5b93202e8c9f14ebcb
# Parent  314246c6eeaa5d1ed84d9e2db97dcb1db5099fc0
clarified Session.Phase;

diff -r 314246c6eeaa -r ff8c3c29a924 src/Pure/PIDE/batch_session.scala
--- a/src/Pure/PIDE/batch_session.scala	Sun Mar 12 19:06:10 2017 +0100
+++ b/src/Pure/PIDE/batch_session.scala	Mon Mar 13 12:04:11 2017 +0100
@@ -46,7 +46,7 @@
           val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
           batch_session.build_theories_result =
             Some(Build.build_theories(prover_session, master_dir, theories))
-        case Session.Inactive | Session.Failed =>
+        case Session.Terminated(_) =>
           batch_session.session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
         case Session.Shutdown =>
           batch_session.session_result.fulfill(())
diff -r 314246c6eeaa -r ff8c3c29a924 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun Mar 12 19:06:10 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Mon Mar 13 12:04:11 2017 +0100
@@ -68,11 +68,18 @@
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
   sealed abstract class Phase
+  {
+    def print: String =
+      this match {
+        case Terminated(rc) => if (rc == 0) "finished" else "failed"
+        case _ => Word.lowercase(this.toString)
+      }
+  }
   case object Inactive extends Phase
   case object Startup extends Phase  // transient
-  case object Failed extends Phase
   case object Ready extends Phase
   case object Shutdown extends Phase  // transient
+  case class Terminated(rc: Int) extends Phase
   //}}}
 
 
@@ -487,8 +494,7 @@
               phase = Session.Ready
 
             case Markup.Return_Code(rc) if output.is_exit =>
-              if (rc == 0) phase = Session.Inactive
-              else phase = Session.Failed
+              phase = Session.Terminated(rc)
               prover.reset
 
             case _ =>
@@ -522,9 +528,11 @@
             all_messages.post(input)
 
           case Start(start_prover) if !prover.defined =>
-            if (phase == Session.Inactive || phase == Session.Failed) {
-              phase = Session.Startup
-              prover.set(start_prover(manager.send(_)))
+            phase match {
+              case Session.Inactive | Session.Terminated(_) =>
+                phase = Session.Startup
+                prover.set(start_prover(manager.send(_)))
+              case _ =>
             }
 
           case Stop =>
diff -r 314246c6eeaa -r ff8c3c29a924 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Sun Mar 12 19:06:10 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Mon Mar 13 12:04:11 2017 +0100
@@ -239,7 +239,7 @@
             session.phase_changed -= session_phase
             session.update_options(options)
             reply("")
-          case Session.Failed =>
+          case Session.Terminated(rc) if rc != 0 =>
             session.phase_changed -= session_phase
             reply("Prover startup failed")
           case _ =>
@@ -267,7 +267,7 @@
         var session_phase: Session.Consumer[Session.Phase] = null
         session_phase =
           Session.Consumer(getClass.getName) {
-            case Session.Inactive =>
+            case Session.Terminated(_) =>
               session.phase_changed -= session_phase
               session.commands_changed -= prover_output
               session.all_messages -= syslog
diff -r 314246c6eeaa -r ff8c3c29a924 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Mar 12 19:06:10 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Mar 13 12:04:11 2017 +0100
@@ -241,7 +241,7 @@
 
   private val session_phase =
     Session.Consumer[Session.Phase](getClass.getName) {
-      case Session.Inactive | Session.Failed =>
+      case Session.Terminated(_) =>
         GUI_Thread.later {
           GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
             "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
diff -r 314246c6eeaa -r ff8c3c29a924 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Mar 12 19:06:10 2017 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Mar 13 12:04:11 2017 +0100
@@ -59,8 +59,7 @@
 
   /* controls */
 
-  def phase_text(phase: Session.Phase): String =
-    "Prover: " + Word.lowercase(phase.toString)
+  def phase_text(phase: Session.Phase): String = "Prover: " + phase.print
 
   private val session_phase = new Label(phase_text(PIDE.session.phase))
   session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)