# HG changeset patch
# User wenzelm
# Date 1338316720 -7200
# Node ID b941dd7df92ac4ea45db005f3b1a8933745803c8
# Parent  9f7b27635b572bd1c92ae97b347b47d7f2911811
make double sure that GUI components are up-to-date after init;

diff -r 9f7b27635b57 -r b941dd7df92a src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Tue May 29 20:20:32 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Tue May 29 20:38:40 2012 +0200
@@ -64,6 +64,11 @@
   session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   session_phase.tooltip = "Prover status"
 
+  private def handle_phase(phase: Session.Phase)
+  {
+    Swing_Thread.later { session_phase.text = " " + phase.toString + " " }
+  }
+
   private val cancel = new Button("Cancel") {
     reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
   }
@@ -173,8 +178,7 @@
               if (text != syslog.text) syslog.text = text
             }
 
-        case phase: Session.Phase =>
-          Swing_Thread.later { session_phase.text = " " + phase.toString + " " }
+        case phase: Session.Phase => handle_phase(phase)
 
         case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
 
@@ -183,17 +187,22 @@
     }
   }
 
-  override def init() {
+  override def init()
+  {
     Isabelle.session.syslog_messages += main_actor
     Isabelle.session.phase_changed += main_actor
+    handle_phase(Isabelle.session.phase)
     Isabelle.session.commands_changed += main_actor
+    handle_update()
   }
 
-  override def exit() {
+  override def exit()
+  {
     Isabelle.session.syslog_messages -= main_actor
     Isabelle.session.phase_changed -= main_actor
     Isabelle.session.commands_changed -= main_actor
   }
 
+  handle_phase(Isabelle.session.phase)
   handle_update()
 }