src/Tools/jEdit/src/sledgehammer_dockable.scala

--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 17 22:08:21 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 17 22:15:45 2013 +0200
@@ -71,6 +71,24 @@
   })
 
 
+  /* provers according to ML */
+
+  private def update_provers()
+  {
+    val new_provers = Sledgehammer_Params.get_provers(PIDE.session)
+    if (new_provers != "" && provers.getText == "") {
+      provers.setText(new_provers)
+      if (provers.getCaret != null)
+        provers.getCaret.setDot(0)
+    }
+  }
+
+  private def query_provers()
+  {
+    PIDE.session.protocol_command("Sledgehammer.provers")
+  }
+
+
   /* main actor */
 
   private val main_actor = actor {
@@ -78,6 +96,10 @@
       react {
         case _: Session.Global_Options =>
           Swing_Thread.later { handle_resize() }
+          query_provers()
+        case Session.Ready => query_provers()
+        case Sledgehammer_Params.Provers =>
+          Swing_Thread.later { update_provers() }
         case bad =>
           java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
       }
@@ -88,7 +110,10 @@
   {
     Swing_Thread.require()
 
+    PIDE.session.phase_changed += main_actor
     PIDE.session.global_options += main_actor
+    Sledgehammer_Params.provers += main_actor
+    if (PIDE.session.is_ready) query_provers()
     handle_resize()
     sledgehammer.activate()
   }
@@ -98,7 +123,9 @@
     Swing_Thread.require()
 
     sledgehammer.deactivate()
+    PIDE.session.phase_changed -= main_actor
     PIDE.session.global_options -= main_actor
+    Sledgehammer_Params.provers -= main_actor
     delay_resize.revoke()
   }
 
@@ -120,7 +147,7 @@
       super.processKeyEvent(evt)
     }
     setToolTipText(provers_label.tooltip)
-    setColumns(20)
+    setColumns(30)
   }
 
   private val timeout = new TextField("30.0", 5) {