941 else |
941 else |
942 error "Nitpick was interrupted." |
942 error "Nitpick was interrupted." |
943 |
943 |
944 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n |
944 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n |
945 step subst orig_assm_ts orig_t = |
945 step subst orig_assm_ts orig_t = |
946 let |
946 let val warning_m = if auto then K () else warning in |
947 val warning_m = if auto then K () else warning |
|
948 val unknown_outcome = ("unknown", state) |
|
949 in |
|
950 if getenv "KODKODI" = "" then |
947 if getenv "KODKODI" = "" then |
|
948 (* The "expect" argument is deliberately ignored if Kodkodi is missing so |
|
949 that the "Nitpick_Examples" can be processed on any machine. *) |
951 (warning_m (Pretty.string_of (plazy install_kodkodi_message)); |
950 (warning_m (Pretty.string_of (plazy install_kodkodi_message)); |
952 unknown_outcome) |
951 ("no_kodkodi", state)) |
953 else |
952 else |
954 let |
953 let |
|
954 val unknown_outcome = ("unknown", state) |
955 val deadline = Option.map (curry Time.+ (Time.now ())) timeout |
955 val deadline = Option.map (curry Time.+ (Time.now ())) timeout |
956 val outcome as (outcome_code, _) = |
956 val outcome as (outcome_code, _) = |
957 time_limit (if debug then NONE else timeout) |
957 time_limit (if debug then NONE else timeout) |
958 (pick_them_nits_in_term deadline state params auto i n step subst |
958 (pick_them_nits_in_term deadline state params auto i n step subst |
959 orig_assm_ts) orig_t |
959 orig_assm_ts) orig_t |