structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
uniform interpretation of ATP_Manager.atps via ATP_Manager.get_atps;

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Oct 14 23:44:37 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 15 00:55:29 2009 +0200
@@ -286,8 +286,8 @@
 
 fun get_atp thy args =
   AList.lookup (op =) args proverK
-  |> the_default (hd (space_explode " " (ATP_Manager.get_atps ())))
-  |> (fn name => (name, the (ATP_Manager.get_prover name thy)))
+  |> the_default (hd (ATP_Manager.get_atps ()))  (* FIXME partial *)
+  |> (fn name => (name, the (ATP_Manager.get_prover name thy)))  (* FIXME partial *)
 
 local
 
@@ -301,8 +301,7 @@
     val (ctxt, goal) = Proof.get_goal st
     val ctxt' = if is_none dir then ctxt
       else Config.put ATP_Wrapper.destdir (the dir) ctxt
-    val atp = prover (ATP_Wrapper.atp_problem_of_goal
-      (ATP_Manager.get_full_types ()) 1 (ctxt', goal))
+    val atp = prover (ATP_Wrapper.atp_problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal))
 
     val time_limit =
       (case hard_timeout of
@@ -448,7 +447,7 @@
 
 fun invoke args =
   let
-    val _ = ATP_Manager.set_full_types (AList.defined (op =) args full_typesK)
+    val _ = ATP_Manager.full_types := AList.defined (op =) args full_typesK
   in Mirabelle.register (init, sledgehammer_action args, done) end
 
 end

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 14 23:44:37 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 00:55:29 2009 +0200
@@ -10,14 +10,11 @@
 
 signature ATP_MANAGER =
 sig
-  val get_atps: unit -> string
-  val set_atps: string -> unit
-  val get_max_atps: unit -> int
-  val set_max_atps: int -> unit
-  val get_timeout: unit -> int
-  val set_timeout: int -> unit
-  val get_full_types: unit -> bool
-  val set_full_types: bool -> unit
+  val atps: string Unsynchronized.ref
+  val get_atps: unit -> string list
+  val max_atps: int Unsynchronized.ref
+  val timeout: int Unsynchronized.ref
+  val full_types: bool Unsynchronized.ref
   val kill: unit -> unit
   val info: unit -> unit
   val messages: int option -> unit
@@ -35,27 +32,13 @@
 val message_store_limit = 20;
 val message_display_limit = 5;
 
-local
+val atps = Unsynchronized.ref "e spass remote_vampire";
+fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps);
 
-val atps = Unsynchronized.ref "e spass remote_vampire";
 val max_atps = Unsynchronized.ref 5;   (* ~1 means infinite number of atps *)
 val timeout = Unsynchronized.ref 60;
 val full_types = Unsynchronized.ref false;
 
-in
-
-fun get_atps () = CRITICAL (fn () => ! atps);
-fun set_atps str = CRITICAL (fn () => atps := str);
-
-fun get_max_atps () = CRITICAL (fn () => ! max_atps);
-fun set_max_atps number = CRITICAL (fn () => max_atps := number);
-
-fun get_timeout () = CRITICAL (fn () => ! timeout);
-fun set_timeout time = CRITICAL (fn () => timeout := time);
-
-fun get_full_types () = CRITICAL (fn () => ! full_types);
-fun set_full_types bool = CRITICAL (fn () => full_types := bool);
-
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_proof
     (Preferences.string_pref atps
@@ -76,8 +59,6 @@
     (Preferences.bool_pref full_types
       "ATP: full types" "ATPs will use full type information");
 
-end;
-
 
 
 (** thread management **)
@@ -144,7 +125,7 @@
 (* kill excessive atp threads *)
 
 fun excessive_atps active =
-  let val max = get_max_atps ()
+  let val max = ! max_atps
   in length active > max andalso max > ~1 end;
 
 local
@@ -337,16 +318,16 @@
         val _ = SimpleThread.fork true (fn () =>
           let
             val _ = register birthtime deadtime (Thread.self (), desc)
-            val problem = ATP_Wrapper.atp_problem_of_goal (get_full_types ()) i
-              (Proof.get_goal proof_state)
+            val problem =
+              ATP_Wrapper.atp_problem_of_goal (! full_types) i (Proof.get_goal proof_state)
             val result =
               let val ATP_Wrapper.Prover_Result {success, message, ...} =
-                prover problem (get_timeout ())
+                prover problem (! timeout)
               in (success, message) end
-              handle ResHolClause.TOO_TRIVIAL
-                => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
-              | ERROR msg
-                => (false, "Error: " ^ msg)
+              handle ResHolClause.TOO_TRIVIAL =>   (* FIXME !? *)
+                  (true, "Empty clause: Try this command: " ^
+                    Markup.markup Markup.sendback "apply metis")
+                | ERROR msg => (false, "Error: " ^ msg)
             val _ = unregister result (Thread.self ())
           in () end handle Interrupt => ())
       in () end);
@@ -356,11 +337,9 @@
 
 fun sledgehammer names proof_state =
   let
-    val provers =
-      if null names then String.tokens (Symbol.is_ascii_blank o String.str) (get_atps ())
-      else names
+    val provers = if null names then get_atps () else names
     val birthtime = Time.now ()
-    val deadtime = Time.+ (birthtime, Time.fromSeconds (get_timeout ()))
+    val deadtime = Time.+ (birthtime, Time.fromSeconds (! timeout))
   in List.app (fn name => start_prover name birthtime deadtime 1 proof_state) provers end;
 
 

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Oct 14 23:44:37 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Oct 15 00:55:29 2009 +0200
@@ -126,7 +126,7 @@
     val _ = debug_fn (fn () => print_names name_thm_pairs)
     val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     val problem = ATP_Wrapper.ATP_Problem {
-      with_full_types = ATP_Manager.get_full_types (),
+      with_full_types = ! ATP_Manager.full_types,
       subgoal = subgoalno,
       goal = Proof.get_goal state,
       axiom_clauses = SOME axclauses,