# HG changeset patch
# User blanchet
# Date 1272032135 -7200
# Node ID 8c83ea1a7740b6d98f9a5dfbbf5379b015a3f3e1
# Parent  a4f601daa17516e8b373e6d0471c46233349508a
move the Sledgehammer menu options to "sledgehammer_isar.ML"

diff -r a4f601daa175 -r 8c83ea1a7740 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Apr 23 15:48:34 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Apr 23 16:15:35 2010 +0200
@@ -49,9 +49,6 @@
   type prover =
     params -> minimize_command -> Time.time -> problem -> prover_result
 
-  val atps: string Unsynchronized.ref
-  val timeout: int Unsynchronized.ref
-  val full_types: bool Unsynchronized.ref
   val kill_atps: unit -> unit
   val running_atps: unit -> unit
   val messages: int option -> unit
@@ -121,26 +118,6 @@
 val message_store_limit = 20;
 val message_display_limit = 5;
 
-val atps = Unsynchronized.ref ""; (* set in "ATP_Wrapper" *)
-val timeout = Unsynchronized.ref 60;
-val full_types = Unsynchronized.ref false;
-
-val _ =
-  ProofGeneralPgip.add_preference Preferences.category_proof
-    (Preferences.string_pref atps
-      "ATP: provers" "Default automatic provers (separated by whitespace)");
-
-val _ =
-  ProofGeneralPgip.add_preference Preferences.category_proof
-    (Preferences.int_pref timeout
-      "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
-
-val _ =
-  ProofGeneralPgip.add_preference Preferences.category_proof
-    (Preferences.bool_pref full_types
-      "ATP: full types" "ATPs will use full type information");
-
-
 
 (** thread management **)
 
diff -r a4f601daa175 -r 8c83ea1a7740 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 23 15:48:34 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 23 16:15:35 2010 +0200
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Tools/ATP_Manager/atp_wrapper.ML
     Author:     Fabian Immler, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
 
 Wrapper functions for external ATPs.
 *)
@@ -14,6 +15,7 @@
   val measure_runtime : bool Config.T
 
   val refresh_systems_on_tptp : unit -> unit
+  val default_atps_param_value : unit -> string
   val setup : theory -> theory
 end;
 
@@ -389,6 +391,13 @@
   tptp_prover (remotify (fst spass))
               (remote_prover_config "SPASS---" "-x" spass_config)
 
+fun maybe_remote (name, _) ({home, ...} : prover_config) =
+  name |> home = "" ? remotify
+
+fun default_atps_param_value () =
+  space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
+                     remotify (fst vampire)]
+
 val provers =
   [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e]
 val prover_setup = fold add_prover provers
@@ -397,11 +406,6 @@
   destdir_setup
   #> problem_prefix_setup
   #> measure_runtime_setup
-  #> prover_setup;
+  #> prover_setup
 
-fun maybe_remote (name, _) ({home, ...} : prover_config) =
-  name |> home = "" ? remotify
-
-val _ = atps := ([maybe_remote e e_config, maybe_remote spass spass_config,
-                  remotify (fst vampire)] |> space_implode " ")
 end;
diff -r a4f601daa175 -r 8c83ea1a7740 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 23 15:48:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 23 16:15:35 2010 +0200
@@ -8,6 +8,9 @@
 sig
   type params = ATP_Manager.params
 
+  val atps: string Unsynchronized.ref
+  val timeout: int Unsynchronized.ref
+  val full_types: bool Unsynchronized.ref
   val default_params : theory -> (string * string) list -> params
 end;
 
@@ -35,6 +38,29 @@
 fun merge_relevance_overrides rs =
   fold merge_relevance_override_pairwise rs (only_relevance_override [])
 
+(*** parameters ***)
+
+val atps = Unsynchronized.ref (default_atps_param_value ())
+val timeout = Unsynchronized.ref 60
+val full_types = Unsynchronized.ref false
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_proof
+      (Preferences.string_pref atps
+          "Sledgehammer: ATPs"
+          "Default automatic provers (separated by whitespace)")
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_proof
+      (Preferences.int_pref timeout
+          "Sledgehammer: Time limit"
+          "ATPs will be interrupted after this time (in seconds)")
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_proof
+      (Preferences.bool_pref full_types
+          "Sledgehammer: Full types" "ATPs will use full type information")
+
 type raw_param = string * string list
 
 val default_default_params =