src/Tools/solve_direct.ML
changeset 52639 df830310e550
parent 52017 bc0238c1f73a
child 52641 c56b6fa636e8
--- a/src/Tools/solve_direct.ML	Fri Jul 12 22:49:20 2013 +0200
+++ b/src/Tools/solve_direct.ML	Fri Jul 12 23:45:05 2013 +0200
@@ -14,7 +14,6 @@
   val someN: string
   val noneN: string
   val unknownN: string
-  val auto: bool Unsynchronized.ref
   val max_solutions: int Unsynchronized.ref
   val solve_direct: Proof.state -> bool * (string * Proof.state)
   val setup: theory -> theory
@@ -33,13 +32,12 @@
 
 (* preferences *)
 
-val auto = Unsynchronized.ref false;
 val max_solutions = Unsynchronized.ref 5;
 
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_tracing
+  ProofGeneral.preference_option ProofGeneral.category_tracing
     (SOME "true")
-    auto
+    @{option auto_solve_direct}
     "auto-solve-direct"
     ("Run " ^ quote solve_directN ^ " automatically");
 
@@ -117,6 +115,6 @@
 
 fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
 
-val setup = Try.register_tool (solve_directN, (10, auto, try_solve_direct));
+val setup = Try.register_tool (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
 
 end;