# HG changeset patch
# User wenzelm
# Date 1397929922 -7200
# Node ID 4675df68450eb8757d6831935694b8f793b6d668
# Parent  891d1b8b64fb7655b5d531350c3d19551ed0f74d
more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);

diff -r 891d1b8b64fb -r 4675df68450e src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Apr 19 19:03:32 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Apr 19 19:52:02 2014 +0200
@@ -498,13 +498,4 @@
         in () end
     | NONE => error "Unknown proof context"))
 
-val _ = Session.protocol_handler "isabelle.Sledgehammer_Params$Handler"
-
-val _ = Isabelle_Process.protocol_command "Sledgehammer.provers"
-  (fn [] =>
-    let
-      val this_thy = @{theory}
-      val provers = space_implode " " (#provers (default_params this_thy []))
-    in Output.protocol_message Markup.sledgehammer_provers [provers] end)
-
 end;
diff -r 891d1b8b64fb -r 4675df68450e src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Sat Apr 19 19:03:32 2014 +0200
+++ b/src/HOL/Tools/etc/options	Sat Apr 19 19:52:02 2014 +0200
@@ -26,6 +26,9 @@
 
 section "Miscellaneous Tools"
 
+public option sledgehammer_provers : string = "e spass remote_vampire"
+  -- "ATPs for Sledgehammer (separated by blanks)"
+
 public option sledgehammer_timeout : int = 30
   -- "ATPs will be interrupted after this time (in seconds)"
 
diff -r 891d1b8b64fb -r 4675df68450e src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Apr 19 19:03:32 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Apr 19 19:52:02 2014 +0200
@@ -178,7 +178,6 @@
   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
@@ -568,8 +567,6 @@
 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");
diff -r 891d1b8b64fb -r 4675df68450e src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Apr 19 19:03:32 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Apr 19 19:52:02 2014 +0200
@@ -399,9 +399,6 @@
       }
   }
 
-  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] =
diff -r 891d1b8b64fb -r 4675df68450e src/Pure/Tools/sledgehammer_params.scala
--- a/src/Pure/Tools/sledgehammer_params.scala	Sat Apr 19 19:03:32 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-/*  Title:      Pure/Tools/sledgehammer_params.scala
-    Author:     Makarius
-
-Protocol for Sledgehammer parameters from ML (see also
-HOL/Tools/Sledgehammer/sledgehammer_commands.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: Prover, msg: Prover.Protocol_Output): Boolean =
-    {
-      update_provers(msg.text)
-      true
-    }
-
-    val functions =
-      Map(Markup.SLEDGEHAMMER_PROVERS -> sledgehammer_provers _)
-  }
-}
diff -r 891d1b8b64fb -r 4675df68450e src/Pure/build-jars
--- a/src/Pure/build-jars	Sat Apr 19 19:03:32 2014 +0200
+++ b/src/Pure/build-jars	Sat Apr 19 19:52:02 2014 +0200
@@ -85,7 +85,6 @@
   Tools/main.scala
   Tools/ml_statistics.scala
   Tools/simplifier_trace.scala
-  Tools/sledgehammer_params.scala
   Tools/task_statistics.scala
   library.scala
   package.scala
diff -r 891d1b8b64fb -r 4675df68450e 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