# HG changeset patch
# User wenzelm
# Date 1285353218 -7200
# Node ID f4da0428dc786076075bf7fe4990569ad64f011f
# Parent  1906c0c773415542b32e9a88ea2e01d2fef3722d
more informative Session.Phase;

diff -r 1906c0c77341 -r f4da0428dc78 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Sep 24 17:55:32 2010 +0200
+++ b/src/Pure/System/session.scala	Fri Sep 24 20:33:38 2010 +0200
@@ -24,7 +24,7 @@
 
   sealed abstract class Phase
   case object Inactive extends Phase
-  case object Exit extends Phase
+  case object Startup extends Phase
   case object Ready extends Phase
   case object Shutdown extends Phase
 }
@@ -209,10 +209,7 @@
           if (result.is_syslog) {
             reverse_syslog ::= result.message
             if (result.is_ready) phase = Session.Ready
-            else if (result.is_exit) {
-              phase = Session.Exit
-              phase = Session.Inactive
-            }
+            else if (result.is_exit) phase = Session.Inactive
           }
           else if (result.is_stdout) { }
           else if (result.is_status) {
@@ -260,6 +257,7 @@
         case result: Isabelle_Process.Result => handle_result(result)
 
         case Start(timeout, args) if prover == null =>
+          phase = Session.Startup
           prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
 
         case Stop if phase == Session.Ready =>
diff -r 1906c0c77341 -r f4da0428dc78 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Sep 24 17:55:32 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Fri Sep 24 20:33:38 2010 +0200
@@ -262,7 +262,7 @@
   private val session_manager = actor {
     loop {
       react {
-        case (Session.Inactive, Session.Exit) =>
+        case (Session.Startup, Session.Inactive) =>
           val text = new scala.swing.TextArea(Isabelle.session.syslog())
           text.editable = false
           Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
diff -r 1906c0c77341 -r f4da0428dc78 src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Fri Sep 24 17:55:32 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Fri Sep 24 20:33:38 2010 +0200
@@ -79,7 +79,7 @@
             }
 
         case (_, phase: Session.Phase) =>
-          Swing_Thread.now { session_phase.text = phase.toString }
+          Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
 
         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
       }