give the inner timeout mechanism a chance, since it gives more precise information to the user
authorblanchet
Tue Dec 07 11:56:01 2010 +0100 (2010-12-07)
changeset 410512ed1b971fc20
parent 41050 effbaa323cf0
child 41052 3db267a01c1d
give the inner timeout mechanism a chance, since it gives more precise information to the user
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:01 2010 +0100
     1.3 @@ -233,8 +233,7 @@
     1.4      val print_v = pprint_v o K o plazy
     1.5  
     1.6      fun check_deadline () =
     1.7 -      if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut
     1.8 -      else ()
     1.9 +      if passed_deadline deadline then raise TimeLimit.TimeOut else ()
    1.10  
    1.11      val assm_ts = if assms orelse auto then assm_ts else []
    1.12      val _ =
    1.13 @@ -981,6 +980,9 @@
    1.14                  ".")
    1.15    in (outcome_code, !state_ref) end
    1.16  
    1.17 +(* Give the inner timeout a chance. *)
    1.18 +val timeout_bonus = seconds 0.25
    1.19 +
    1.20  fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
    1.21                        step subst assm_ts orig_t =
    1.22    let val warning_m = if auto then K () else warning in
    1.23 @@ -994,7 +996,8 @@
    1.24          val unknown_outcome = ("unknown", state)
    1.25          val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    1.26          val outcome as (outcome_code, _) =
    1.27 -          time_limit (if debug then NONE else timeout)
    1.28 +          time_limit (if debug orelse is_none timeout then NONE
    1.29 +                      else SOME (Time.+ (the timeout, timeout_bonus)))
    1.30                (pick_them_nits_in_term deadline state params auto i n step subst
    1.31                                        assm_ts) orig_t
    1.32            handle TOO_LARGE (_, details) =>