equal
deleted
inserted
replaced
978 (print_m (fn () => excipit "ran out of time after checking"); |
978 (print_m (fn () => excipit "ran out of time after checking"); |
979 if !met_potential > 0 then "potential" else "unknown") |
979 if !met_potential > 0 then "potential" else "unknown") |
980 | Exn.Interrupt => |
980 | Exn.Interrupt => |
981 if auto orelse debug then raise Interrupt |
981 if auto orelse debug then raise Interrupt |
982 else error (excipit "was interrupted after checking") |
982 else error (excipit "was interrupted after checking") |
983 val _ = print_v (fn () => "Total time: " ^ |
983 val _ = print_v (fn () => |
984 signed_string_of_int (Time.toMilliseconds |
984 "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^ |
985 (Timer.checkRealTimer timer)) ^ " ms.") |
985 ".") |
986 in (outcome_code, !state_ref) end |
986 in (outcome_code, !state_ref) end |
987 handle Exn.Interrupt => |
987 handle Exn.Interrupt => |
988 if auto orelse #debug params then |
988 if auto orelse #debug params then |
989 raise Interrupt |
989 raise Interrupt |
990 else |
990 else |