--- a/src/Tools/auto_tools.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/Tools/auto_tools.ML Fri Dec 03 09:55:45 2010 +0100
@@ -6,10 +6,11 @@
signature AUTO_TOOLS =
sig
- val time_limit: int Unsynchronized.ref
+ val time_limit: real Unsynchronized.ref
val register_tool :
- string * (Proof.state -> bool * Proof.state) -> theory -> theory
+ bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
+ -> theory
end;
structure Auto_Tools : AUTO_TOOLS =
@@ -17,20 +18,20 @@
(* preferences *)
-val time_limit = Unsynchronized.ref 4000
+val time_limit = Unsynchronized.ref 4.0
+val auto_tools_time_limitN = "auto-tools-time-limit"
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.nat_pref time_limit
- "auto-tools-time-limit"
- "Time limit for automatic tools (in milliseconds).")
+ (Preferences.real_pref time_limit
+ auto_tools_time_limitN "Time limit for automatic tools (in seconds).")
(* configuration *)
structure Data = Theory_Data
(
- type T = (string * (Proof.state -> bool * Proof.state)) list
+ type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list
val empty = []
val extend = I
fun merge data : T = AList.merge (op =) (K true) data
@@ -41,18 +42,30 @@
(* automatic testing *)
+fun run_tools tools state =
+ tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
+ |> Par_List.get_some (fn tool =>
+ case try tool state of
+ SOME (true, state) => SOME state
+ | _ => NONE)
+ |> the_default state
+
+(* Too large values are understood as milliseconds, ensuring compatibility with
+ old setting files. No users can possibly in their right mind want the user
+ interface to block for more than 100 seconds. *)
+fun smart_seconds r =
+ seconds (if r >= 100.0 then
+ (legacy_feature (quote auto_tools_time_limitN ^
+ " expressed in milliseconds -- use seconds instead"); 0.001 * r)
+ else
+ r)
+
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
- case !time_limit of
- 0 => state
- | ms =>
- TimeLimit.timeLimit (Time.fromMilliseconds ms)
- (fn () =>
- if interact andalso not (!Toplevel.quiet) then
- fold_rev (fn (_, tool) => fn (true, state) => (true, state)
- | (false, state) => tool state)
- (Data.get (Proof.theory_of state)) (false, state) |> snd
- else
- state) ()
- handle TimeLimit.TimeOut => state))
+ if interact andalso not (!Toplevel.quiet) andalso !time_limit > 0.0 then
+ TimeLimit.timeLimit (smart_seconds (!time_limit))
+ (run_tools (Data.get (Proof.theory_of state))) state
+ handle TimeLimit.TimeOut => state
+ else
+ state))
end;