58 |
58 |
59 (* try command *) |
59 (* try command *) |
60 |
60 |
61 fun try_tools state = |
61 fun try_tools state = |
62 if subgoal_count state = 0 then |
62 if subgoal_count state = 0 then |
63 (Output.urgent_message "No subgoal!"; NONE) |
63 (writeln "No subgoal!"; NONE) |
64 else |
64 else |
65 get_tools (Proof.theory_of state) |
65 get_tools (Proof.theory_of state) |
66 |> tap (fn tools => |
66 |> tap (fn tools => |
67 "Trying " ^ space_implode " " |
67 "Trying " ^ space_implode " " |
68 (serial_commas "and" (map (quote o fst) tools)) ^ "..." |
68 (serial_commas "and" (map (quote o fst) tools)) ^ "..." |
69 |> Output.urgent_message) |
69 |> writeln) |
70 |> Par_List.get_some |
70 |> Par_List.get_some |
71 (fn (name, (_, _, tool)) => |
71 (fn (name, (_, _, tool)) => |
72 case try (tool false) state of |
72 case try (tool false) state of |
73 SOME (true, (outcome_code, _)) => SOME (name, outcome_code) |
73 SOME (true, (outcome_code, _)) => SOME (name, outcome_code) |
74 | _ => NONE) |
74 | _ => NONE) |
75 |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ()) |
75 |> tap (fn NONE => writeln "Tried in vain." | _ => ()) |
76 |
76 |
77 val _ = |
77 val _ = |
78 Outer_Syntax.improper_command @{command_spec "try"} |
78 Outer_Syntax.improper_command @{command_spec "try"} |
79 "try a combination of automatic proving and disproving tools" |
79 "try a combination of automatic proving and disproving tools" |
80 (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) |
80 (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) |