src/Tools/jEdit/src/jedit/session_dockable.scala
changeset 39635 5cd8545a070b
parent 39629 08eb2730a8a1
child 39638 4293ce5b07fb
     1.1 --- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 23:04:50 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Fri Sep 24 00:00:21 2010 +0200
     1.3 @@ -10,7 +10,8 @@
     1.4  import isabelle._
     1.5  
     1.6  import scala.actors.Actor._
     1.7 -import scala.swing.{FlowPanel, Button, TextArea, ScrollPane, TabbedPane, Component}
     1.8 +import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane,
     1.9 +  Component, Swing}
    1.10  import scala.swing.event.ButtonClicked
    1.11  
    1.12  import java.awt.BorderLayout
    1.13 @@ -38,12 +39,17 @@
    1.14  
    1.15    /* controls */
    1.16  
    1.17 +  val session_phase = new Label(Isabelle.session.phase.toString)
    1.18 +  session_phase.border = Swing.EtchedBorder(Swing.Lowered)
    1.19 +  session_phase.tooltip = "Prover process status"
    1.20 +
    1.21    private val interrupt = new Button("Interrupt") {
    1.22      reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
    1.23    }
    1.24    interrupt.tooltip = "Broadcast interrupt to all prover tasks"
    1.25  
    1.26 -  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(interrupt)
    1.27 +  private val controls =
    1.28 +    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt)
    1.29    add(controls.peer, BorderLayout.NORTH)
    1.30  
    1.31  
    1.32 @@ -61,11 +67,21 @@
    1.33                }
    1.34              }
    1.35  
    1.36 +        case (_, phase: Session.Phase) =>
    1.37 +          Swing_Thread.now { session_phase.text = phase.toString }
    1.38 +
    1.39          case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
    1.40        }
    1.41      }
    1.42    }
    1.43  
    1.44 -  override def init() { Isabelle.session.raw_messages += main_actor }
    1.45 -  override def exit() { Isabelle.session.raw_messages -= main_actor }
    1.46 +  override def init() {
    1.47 +    Isabelle.session.raw_messages += main_actor
    1.48 +    Isabelle.session.phase_changed += main_actor
    1.49 +  }
    1.50 +
    1.51 +  override def exit() {
    1.52 +    Isabelle.session.raw_messages -= main_actor
    1.53 +    Isabelle.session.phase_changed -= main_actor
    1.54 +  }
    1.55  }