# HG changeset patch
# User wenzelm
# Date 1285279221 -7200
# Node ID 5cd8545a070bc760de664e8e32bcf072835967d6
# Parent  4030a9ef9c5a505b21b78c5c75a08eed81eaea35
added Session_Dockable.session_phase label;

diff -r 4030a9ef9c5a -r 5cd8545a070b src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 23:04:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Fri Sep 24 00:00:21 2010 +0200
@@ -10,7 +10,8 @@
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, ScrollPane, TabbedPane, Component}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane,
+  Component, Swing}
 import scala.swing.event.ButtonClicked
 
 import java.awt.BorderLayout
@@ -38,12 +39,17 @@
 
   /* controls */
 
+  val session_phase = new Label(Isabelle.session.phase.toString)
+  session_phase.border = Swing.EtchedBorder(Swing.Lowered)
+  session_phase.tooltip = "Prover process status"
+
   private val interrupt = new Button("Interrupt") {
     reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
   }
   interrupt.tooltip = "Broadcast interrupt to all prover tasks"
 
-  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(interrupt)
+  private val controls =
+    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt)
   add(controls.peer, BorderLayout.NORTH)
 
 
@@ -61,11 +67,21 @@
               }
             }
 
+        case (_, phase: Session.Phase) =>
+          Swing_Thread.now { session_phase.text = phase.toString }
+
         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
       }
     }
   }
 
-  override def init() { Isabelle.session.raw_messages += main_actor }
-  override def exit() { Isabelle.session.raw_messages -= main_actor }
+  override def init() {
+    Isabelle.session.raw_messages += main_actor
+    Isabelle.session.phase_changed += main_actor
+  }
+
+  override def exit() {
+    Isabelle.session.raw_messages -= main_actor
+    Isabelle.session.phase_changed -= main_actor
+  }
 }