src/HOL/Tools/Nitpick/nitpick.ML
changeset 62519 a564458f94db
parent 62319 6b01bff94d87
child 62826 eb94e570c1a4
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Mar 05 13:57:25 2016 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Mar 05 17:01:45 2016 +0100
     1.3 @@ -211,6 +211,7 @@
     1.4  fun pick_them_nits_in_term deadline state (params : params) mode i n step
     1.5                             subst def_assm_ts nondef_assm_ts orig_t =
     1.6    let
     1.7 +    val time_start = Time.now ()
     1.8      val timer = Timer.startRealTimer ()
     1.9      val thy = Proof.theory_of state
    1.10      val ctxt = Proof.context_of state
    1.11 @@ -248,10 +249,11 @@
    1.12      val print_v = pprint_v o K o plazy
    1.13  
    1.14      fun check_deadline () =
    1.15 -      if Time.compare (Time.now (), deadline) <> LESS then
    1.16 -        raise TimeLimit.TimeOut
    1.17 -      else
    1.18 -        ()
    1.19 +      let val t = Time.now () in
    1.20 +        if Time.compare (t, deadline) <> LESS
    1.21 +        then raise Timeout.TIMEOUT (Time.- (t, time_start))
    1.22 +        else ()
    1.23 +      end
    1.24  
    1.25      val (def_assm_ts, nondef_assm_ts) =
    1.26        if assms orelse mode <> Normal then (def_assm_ts, nondef_assm_ts)
    1.27 @@ -376,9 +378,9 @@
    1.28         (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
    1.29        is_number_type ctxt T orelse is_bit_type T
    1.30      fun is_type_actually_monotonic T =
    1.31 -      TimeLimit.timeLimit tac_timeout (formulas_monotonic hol_ctxt binarize T)
    1.32 +      Timeout.apply tac_timeout (formulas_monotonic hol_ctxt binarize T)
    1.33                            (nondef_ts, def_ts)
    1.34 -      handle TimeLimit.TimeOut => false
    1.35 +        handle Timeout.TIMEOUT _ => false
    1.36      fun is_type_kind_of_monotonic T =
    1.37        case triple_lookup (type_match thy) monos T of
    1.38          SOME (SOME false) => false
    1.39 @@ -806,7 +808,7 @@
    1.40                  end
    1.41              end
    1.42            | KK.TimedOut unsat_js =>
    1.43 -            (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
    1.44 +            (update_checked_problems problems unsat_js; raise Timeout.TIMEOUT Time.zeroTime)
    1.45            | KK.Error (s, unsat_js) =>
    1.46              (update_checked_problems problems unsat_js;
    1.47               print_v (K ("Kodkod error: " ^ s ^ "."));
    1.48 @@ -958,7 +960,7 @@
    1.49      val outcome_code =
    1.50        run_batches 0 (length batches) batches
    1.51                    (false, max_potential, max_genuine, 0)
    1.52 -      handle TimeLimit.TimeOut =>
    1.53 +      handle Timeout.TIMEOUT _ =>
    1.54               (print_nt (fn () => excipit "ran out of time after checking");
    1.55                if !met_potential > 0 then potentialN else unknownN)
    1.56      val _ = print_v (fn () =>
    1.57 @@ -986,7 +988,7 @@
    1.58          val unknown_outcome = (unknownN, [])
    1.59          val deadline = Time.+ (Time.now (), timeout)
    1.60          val outcome as (outcome_code, _) =
    1.61 -          TimeLimit.timeLimit (Time.+ (timeout, timeout_bonus))
    1.62 +          Timeout.apply (Time.+ (timeout, timeout_bonus))
    1.63                (pick_them_nits_in_term deadline state params mode i n step subst
    1.64                                        def_assm_ts nondef_assm_ts) orig_t
    1.65            handle TOO_LARGE (_, details) =>
    1.66 @@ -999,7 +1001,7 @@
    1.67                   (print_t "% SZS status GaveUp";
    1.68                    print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
    1.69                    unknown_outcome)
    1.70 -               | TimeLimit.TimeOut =>
    1.71 +               | Timeout.TIMEOUT _ =>
    1.72                   (print_t "% SZS status TimedOut";
    1.73                    print_nt "Nitpick ran out of time."; unknown_outcome)
    1.74        in