--- 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
+ }
}