# HG changeset patch
# User wenzelm
# Date 1397930486 -7200
# Node ID 7eed0fee0241c53d733dea503de6718da974287f
# Parent  4675df68450eb8757d6831935694b8f793b6d668
clarified actor plumbing;

diff -r 4675df68450e -r 7eed0fee0241 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Apr 19 19:52:02 2014 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Apr 19 20:01:26 2014 +0200
@@ -69,37 +69,6 @@
   })
 
 
-  /* main actor */
-
-  private val main_actor = actor {
-    loop {
-      react {
-        case _: Session.Global_Options =>
-          Swing_Thread.later { update_provers(); handle_resize() }
-
-        case bad =>
-          System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
-      }
-    }
-  }
-
-  override def init()
-  {
-    PIDE.session.phase_changed += main_actor
-    PIDE.session.global_options += main_actor
-    handle_resize()
-    sledgehammer.activate()
-  }
-
-  override def exit()
-  {
-    sledgehammer.deactivate()
-    PIDE.session.phase_changed -= main_actor
-    PIDE.session.global_options -= main_actor
-    delay_resize.revoke()
-  }
-
-
   /* controls */
 
   private def clicked {
@@ -164,4 +133,34 @@
   add(controls.peer, BorderLayout.NORTH)
 
   override def focusOnDefaultComponent { provers.requestFocus }
+
+
+  /* main actor */
+
+  private val main_actor = actor {
+    loop {
+      react {
+        case _: Session.Global_Options =>
+          Swing_Thread.later { update_provers(); handle_resize() }
+
+        case bad =>
+          System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
+      }
+    }
+  }
+
+  override def init()
+  {
+    PIDE.session.global_options += main_actor
+    update_provers()
+    handle_resize()
+    sledgehammer.activate()
+  }
+
+  override def exit()
+  {
+    sledgehammer.deactivate()
+    PIDE.session.global_options -= main_actor
+    delay_resize.revoke()
+  }
 }