equal
deleted
inserted
replaced
81 ("Timeout", Timeout), |
81 ("Timeout", Timeout), |
82 ("time limit exceeded", Timeout), |
82 ("time limit exceeded", Timeout), |
83 ("# Cannot determine problem status within resource limit", Timeout), |
83 ("# Cannot determine problem status within resource limit", Timeout), |
84 ("Error", Error)] |
84 ("Error", Error)] |
85 |
85 |
86 fun produce_answer (success, message, result_string, thm_name_vec, filtered) = |
86 fun produce_answer (success, message, _, result_string, thm_name_vec, filtered) = |
87 if success then |
87 if success then |
88 (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string) |
88 (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string) |
89 else |
89 else |
90 let |
90 let |
91 val failure = failure_strings |> get_first (fn (s, t) => |
91 val failure = failure_strings |> get_first (fn (s, t) => |