some protocol to determine provers according to ML;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Aug 17 22:08:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Aug 17 22:15:45 2013 +0200
@@ -517,6 +517,15 @@
             run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
               no_fact_override (minimize_command override_params 1) state
         in () end
-    | NONE => error "Unknown proof context"));
+    | NONE => error "Unknown proof context"))
+
+val _ = Session.protocol_handler "isabelle.Sledgehammer_Params$Handler"
+
+val _ = Isabelle_Process.protocol_command "Sledgehammer.provers"
+  (fn [] =>
+    let
+      val this_ctxt = @{context}
+      val provers = space_implode " " (#provers (default_params this_ctxt []))
+    in Output.protocol_message Markup.sledgehammer_provers provers end)
 
 end;

--- a/src/Pure/PIDE/markup.ML	Sat Aug 17 22:08:21 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Aug 17 22:15:45 2013 +0200
@@ -150,6 +150,7 @@
   val protocol_handler: string -> Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
+  val sledgehammer_provers: Properties.T
   val ML_statistics: Properties.entry
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
@@ -480,6 +481,8 @@
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
+val sledgehammer_provers = [(functionN, "sledgehammer_provers")];
+
 val ML_statistics = (functionN, "ML_statistics");
 
 val task_statistics = (functionN, "task_statistics");

--- a/src/Pure/PIDE/markup.scala	Sat Aug 17 22:08:21 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Aug 17 22:15:45 2013 +0200
@@ -353,6 +353,9 @@
       }
   }
 
+  val SLEDGEHAMMER_PROVERS = "sledgehammer_provers"
+  val Sledgehammer_Provers: Properties.T = List((FUNCTION, SLEDGEHAMMER_PROVERS))
+
   object ML_Statistics
   {
     def unapply(props: Properties.T): Option[Properties.T] =

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/sledgehammer_params.scala	Sat Aug 17 22:15:45 2013 +0200
@@ -0,0 +1,52 @@
+/*  Title:      Pure/Tools/sledgehammer_params.scala
+    Author:     Makarius
+
+Protocol for Sledgehammer parameters from ML (see also
+HOL/Tools/Sledgehammer/sledgehammer_isar.ML).  */
+
+package isabelle
+
+
+object Sledgehammer_Params
+{
+  /* global event bus */
+
+  case object Provers
+  val provers = new Event_Bus[Provers.type]
+
+
+  /* per session result */
+
+  def get_provers(session: Session): String =
+    session.protocol_handler("isabelle.Sledgehammer_Params$Handler") match {
+      case Some(handler: Handler) => handler.get_provers
+      case _ => ""
+    }
+
+
+  /* handler */
+
+  class Handler extends Session.Protocol_Handler
+  {
+    private var _provers: String = ""
+    private def update_provers(s: String)
+    {
+      synchronized { _provers = s }
+      provers.event(Provers)
+    }
+    def get_provers: String = synchronized { _provers }
+
+    private def sledgehammer_provers(
+      prover: Session.Prover, output: Isabelle_Process.Output): Boolean =
+    {
+      output.body match {
+        case Nil => update_provers(""); true
+        case List(XML.Text(s)) => update_provers(s); true
+        case _ => false
+      }
+    }
+
+    val functions =
+      Map(Markup.SLEDGEHAMMER_PROVERS -> sledgehammer_provers _)
+  }
+}

--- a/src/Pure/build-jars	Sat Aug 17 22:08:21 2013 +0200
+++ b/src/Pure/build-jars	Sat Aug 17 22:15:45 2013 +0200
@@ -77,6 +77,7 @@
   Tools/keywords.scala
   Tools/main.scala
   Tools/ml_statistics.scala
+  Tools/sledgehammer_params.scala
   Tools/task_statistics.scala
   library.scala
   package.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) {