equal
deleted
inserted
replaced
55 |
55 |
56 (* try command *) |
56 (* try command *) |
57 |
57 |
58 fun try_tools state = |
58 fun try_tools state = |
59 get_tools (Proof.theory_of state) |
59 get_tools (Proof.theory_of state) |
|
60 |> tap (fn _ => Output.urgent_message "Trying...") |
60 |> Par_List.get_some |
61 |> Par_List.get_some |
61 (fn (name, (_, tool)) => |
62 (fn (name, (_, tool)) => |
62 case try (tool false) state of |
63 case try (tool false) state of |
63 SOME (true, (outcome_code, _)) => SOME (name, outcome_code) |
64 SOME (true, (outcome_code, _)) => SOME (name, outcome_code) |
64 | _ => NONE) |
65 | _ => NONE) |