--- a/src/Tools/auto_solve.ML Wed Apr 22 11:00:25 2009 -0700
+++ b/src/Tools/auto_solve.ML Mon Apr 27 07:26:17 2009 -0700
@@ -14,18 +14,34 @@
val auto : bool ref
val auto_time_limit : int ref
val limit : int ref
-
- val seek_solution : bool -> Proof.state -> Proof.state
end;
structure AutoSolve : AUTO_SOLVE =
struct
+(* preferences *)
+
val auto = ref false;
val auto_time_limit = ref 2500;
val limit = ref 5;
-fun seek_solution int state =
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (setmp auto true (fn () =>
+ Preferences.bool_pref auto
+ "auto-solve"
+ "Try to solve newly declared lemmas with existing theorems.") ());
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (Preferences.nat_pref auto_time_limit
+ "auto-solve-time-limit"
+ "Time limit for seeking automatic solutions (in milliseconds).");
+
+
+(* hook *)
+
+val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
let
val ctxt = Proof.context_of state;
@@ -76,12 +92,10 @@
if int andalso ! auto andalso not (! Toplevel.quiet)
then go ()
else state
- end;
+ end));
end;
-val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);
-
val auto_solve = AutoSolve.auto;
val auto_solve_time_limit = AutoSolve.auto_time_limit;