1.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Dec 03 09:55:45 2010 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4  nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
     1.5  refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
     1.6  *)
     1.7 -ML {* Auto_Tools.time_limit := 10 *}
     1.8 +ML {* Auto_Tools.time_limit := 10.0 *}
     1.9  
    1.10  ML {* val mtds = [
    1.11    MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",

     2.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 03 08:40:47 2010 +0100
     2.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 03 09:55:45 2010 +0100
     2.3 @@ -114,13 +114,14 @@
     2.4  (** quickcheck **)
     2.5  
     2.6  fun invoke_quickcheck change_options quickcheck_generator thy t =
     2.7 -  TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
     2.8 +  TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
     2.9        (fn _ =>
    2.10            case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
    2.11                false [] [t] of
    2.12              (NONE, _) => (NoCex, ([], NONE))
    2.13            | (SOME _, _) => (GenuineCex, ([], NONE))) ()
    2.14 -  handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
    2.15 +  handle TimeLimit.TimeOut =>
    2.16 +         (Timeout, ([("timelimit", Real.floor !Auto_Tools.time_limit)], NONE))
    2.17  
    2.18  fun quickcheck_mtd change_options quickcheck_generator =
    2.19    ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Dec 03 08:40:47 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Dec 03 09:55:45 2010 +0100
     3.3 @@ -383,9 +383,8 @@
     3.4              "set and display the default parameters for Nitpick"
     3.5              Keyword.thy_decl parse_nitpick_params_command
     3.6  
     3.7 -fun auto_nitpick state =
     3.8 -  if not (!auto) then (false, state) else pick_nits [] true 1 0 state
     3.9 +val auto_nitpick = pick_nits [] true 1 0
    3.10  
    3.11 -val setup = Auto_Tools.register_tool ("nitpick", auto_nitpick)
    3.12 +val setup = Auto_Tools.register_tool (auto, auto_nitpick)
    3.13  
    3.14  end;

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Dec 03 08:40:47 2010 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Dec 03 09:55:45 2010 +0100
     4.3 @@ -347,14 +347,11 @@
     4.4        parse_sledgehammer_params_command
     4.5  
     4.6  fun auto_sledgehammer state =
     4.7 -  if not (!auto) then
     4.8 -    (false, state)
     4.9 -  else
    4.10 -    let val ctxt = Proof.context_of state in
    4.11 -      run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
    4.12 -                       (minimize_command [] 1) state
    4.13 -    end
    4.14 +  let val ctxt = Proof.context_of state in
    4.15 +    run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
    4.16 +                     (minimize_command [] 1) state
    4.17 +  end
    4.18  
    4.19 -val setup = Auto_Tools.register_tool (sledgehammerN, auto_sledgehammer)
    4.20 +val setup = Auto_Tools.register_tool (auto, auto_sledgehammer)
    4.21  
    4.22  end;

     5.1 --- a/src/HOL/Tools/try.ML	Fri Dec 03 08:40:47 2010 +0100
     5.2 +++ b/src/HOL/Tools/try.ML	Fri Dec 03 09:55:45 2010 +0100
     5.3 @@ -110,8 +110,8 @@
     5.4        (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
     5.5                                      o Toplevel.proof_of)))
     5.6  
     5.7 -fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
     5.8 +val auto_try = do_try true NONE
     5.9  
    5.10 -val setup = Auto_Tools.register_tool (tryN, auto_try)
    5.11 +val setup = Auto_Tools.register_tool (auto, auto_try)
    5.12  
    5.13  end;

     6.1 --- a/src/Tools/auto_tools.ML	Fri Dec 03 08:40:47 2010 +0100
     6.2 +++ b/src/Tools/auto_tools.ML	Fri Dec 03 09:55:45 2010 +0100
     6.3 @@ -6,10 +6,11 @@
     6.4  
     6.5  signature AUTO_TOOLS =
     6.6  sig
     6.7 -  val time_limit: int Unsynchronized.ref
     6.8 +  val time_limit: real Unsynchronized.ref
     6.9  
    6.10    val register_tool :
    6.11 -    string * (Proof.state -> bool * Proof.state) -> theory -> theory
    6.12 +    bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
    6.13 +    -> theory
    6.14  end;
    6.15  
    6.16  structure Auto_Tools : AUTO_TOOLS =
    6.17 @@ -17,20 +18,20 @@
    6.18  
    6.19  (* preferences *)
    6.20  
    6.21 -val time_limit = Unsynchronized.ref 4000
    6.22 +val time_limit = Unsynchronized.ref 4.0
    6.23  
    6.24 +val auto_tools_time_limitN = "auto-tools-time-limit"
    6.25  val _ =
    6.26    ProofGeneralPgip.add_preference Preferences.category_tracing
    6.27 -    (Preferences.nat_pref time_limit
    6.28 -      "auto-tools-time-limit"
    6.29 -      "Time limit for automatic tools (in milliseconds).")
    6.30 +    (Preferences.real_pref time_limit
    6.31 +      auto_tools_time_limitN "Time limit for automatic tools (in seconds).")
    6.32  
    6.33  
    6.34  (* configuration *)
    6.35  
    6.36  structure Data = Theory_Data
    6.37  (
    6.38 -  type T = (string * (Proof.state -> bool * Proof.state)) list
    6.39 +  type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list
    6.40    val empty = []
    6.41    val extend = I
    6.42    fun merge data : T = AList.merge (op =) (K true) data
    6.43 @@ -41,18 +42,30 @@
    6.44  
    6.45  (* automatic testing *)
    6.46  
    6.47 +fun run_tools tools state =
    6.48 +  tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
    6.49 +        |> Par_List.get_some (fn tool =>
    6.50 +                                 case try tool state of
    6.51 +                                   SOME (true, state) => SOME state
    6.52 +                                 | _ => NONE)
    6.53 +        |> the_default state
    6.54 +
    6.55 +(* Too large values are understood as milliseconds, ensuring compatibility with
    6.56 +   old setting files. No users can possibly in their right mind want the user
    6.57 +   interface to block for more than 100 seconds. *)
    6.58 +fun smart_seconds r =
    6.59 +  seconds (if r >= 100.0 then
    6.60 +             (legacy_feature (quote auto_tools_time_limitN ^
    6.61 +                " expressed in milliseconds -- use seconds instead"); 0.001 * r)
    6.62 +           else
    6.63 +             r)
    6.64 +
    6.65  val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
    6.66 -  case !time_limit of
    6.67 -    0 => state
    6.68 -  | ms =>
    6.69 -    TimeLimit.timeLimit (Time.fromMilliseconds ms)
    6.70 -        (fn () =>
    6.71 -            if interact andalso not (!Toplevel.quiet) then
    6.72 -              fold_rev (fn (_, tool) => fn (true, state) => (true, state)
    6.73 -                                         | (false, state) => tool state)
    6.74 -                   (Data.get (Proof.theory_of state)) (false, state) |> snd
    6.75 -            else
    6.76 -              state) ()
    6.77 -    handle TimeLimit.TimeOut => state))
    6.78 +  if interact andalso not (!Toplevel.quiet) andalso !time_limit > 0.0 then
    6.79 +    TimeLimit.timeLimit (smart_seconds (!time_limit))
    6.80 +        (run_tools (Data.get (Proof.theory_of state))) state
    6.81 +    handle TimeLimit.TimeOut => state
    6.82 +  else
    6.83 +    state))
    6.84  
    6.85  end;

     7.1 --- a/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
     7.2 +++ b/src/Tools/quickcheck.ML	Fri Dec 03 09:55:45 2010 +0100
     7.3 @@ -303,24 +303,21 @@
     7.4  (* automatic testing *)
     7.5  
     7.6  fun auto_quickcheck state =
     7.7 -  if not (!auto) then
     7.8 -    (false, state)
     7.9 -  else
    7.10 -    let
    7.11 -      val ctxt = Proof.context_of state;
    7.12 -      val res =
    7.13 -        state
    7.14 -        |> Proof.map_context (Config.put report false #> Config.put quiet true)
    7.15 -        |> try (test_goal [] 1);
    7.16 -    in
    7.17 -      case res of
    7.18 -        NONE => (false, state)
    7.19 -      | SOME (NONE, report) => (false, state)
    7.20 -      | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    7.21 -          Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
    7.22 -    end
    7.23 +  let
    7.24 +    val ctxt = Proof.context_of state;
    7.25 +    val res =
    7.26 +      state
    7.27 +      |> Proof.map_context (Config.put report false #> Config.put quiet true)
    7.28 +      |> try (test_goal [] 1);
    7.29 +  in
    7.30 +    case res of
    7.31 +      NONE => (false, state)
    7.32 +    | SOME (NONE, report) => (false, state)
    7.33 +    | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    7.34 +        Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
    7.35 +  end
    7.36  
    7.37 -val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
    7.38 +val setup = Auto_Tools.register_tool (auto, auto_quickcheck)
    7.39    #> setup_config
    7.40  
    7.41  (* Isar commands *)

     8.1 --- a/src/Tools/solve_direct.ML	Fri Dec 03 08:40:47 2010 +0100
     8.2 +++ b/src/Tools/solve_direct.ML	Fri Dec 03 09:55:45 2010 +0100
     8.3 @@ -97,9 +97,8 @@
     8.4  
     8.5  (* hook *)
     8.6  
     8.7 -fun auto_solve_direct state =
     8.8 -  if not (! auto) then (false, state) else solve_direct true state;
     8.9 +val auto_solve_direct = solve_direct true
    8.10  
    8.11 -val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct);
    8.12 +val setup = Auto_Tools.register_tool (auto, auto_solve_direct);
    8.13  
    8.14  end;