src/Tools/jEdit/src/sledgehammer_dockable.scala

--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Apr 19 19:03:32 2014 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Apr 19 19:52:02 2014 +0200
@@ -69,39 +69,13 @@
   })
 
 
-  /* 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()
-  {
-    if (PIDE.session.is_ready)
-      PIDE.session.protocol_command("Sledgehammer.provers")
-  }
-
-
   /* main actor */
 
   private val main_actor = actor {
     loop {
       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() }
+          Swing_Thread.later { update_provers(); handle_resize() }
 
         case bad =>
           System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
@@ -113,8 +87,6 @@
   {
     PIDE.session.phase_changed += main_actor
     PIDE.session.global_options += main_actor
-    Sledgehammer_Params.provers += main_actor
-    query_provers()
     handle_resize()
     sledgehammer.activate()
   }
@@ -124,7 +96,6 @@
     sledgehammer.deactivate()
     PIDE.session.phase_changed -= main_actor
     PIDE.session.global_options -= main_actor
-    Sledgehammer_Params.provers -= main_actor
     delay_resize.revoke()
   }
 
@@ -132,6 +103,7 @@
   /* controls */
 
   private def clicked {
+    PIDE.options.string("sledgehammer_provers") = provers.getText
     sledgehammer.apply_query(List(provers.getText, isar_proofs.selected.toString))
   }
 
@@ -151,6 +123,16 @@
     setColumns(30)
   }
 
+  private def update_provers()
+  {
+    val new_provers = PIDE.options.string("sledgehammer_provers")
+    if (new_provers != provers.getText) {
+      provers.setText(new_provers)
+      if (provers.getCaret != null)
+        provers.getCaret.setDot(0)
+    }
+  }
+
   private val isar_proofs = new CheckBox("Isar proofs") {
     tooltip = "Specify whether Isar proofs should be output in addition to metis line"
     selected = false