src/Tools/auto_tools.ML

--- 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;