75 val do_methods = map do_named_method named_methods |
75 val do_methods = map do_named_method named_methods |
76 |
76 |
77 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms" |
77 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms" |
78 |
78 |
79 fun do_try auto timeout_opt st = |
79 fun do_try auto timeout_opt st = |
80 case do_methods |> Par_List.map (fn f => f auto timeout_opt st) |
80 let |
81 |> map_filter I |> sort (int_ord o pairself snd) of |
81 val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false) |
82 [] => (if auto then () else writeln "No proof found."; (false, st)) |
82 in |
83 | xs as (s, _) :: _ => |
83 case do_methods |> Par_List.map (fn f => f auto timeout_opt st) |
84 let |
84 |> map_filter I |> sort (int_ord o pairself snd) of |
85 val xs = xs |> map swap |> AList.coalesce (op =) |
85 [] => (if auto then () else writeln "No proof found."; (false, st)) |
86 |> map (swap o apsnd commas) |
86 | xs as (s, _) :: _ => |
87 val message = |
87 let |
88 (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^ |
88 val xs = xs |> map swap |> AList.coalesce (op =) |
89 Markup.markup Markup.sendback |
89 |> map (swap o apsnd commas) |
90 ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ |
90 val message = |
91 " " ^ s) ^ |
91 (if auto then "Auto Try found a proof" else "Try this command") ^ |
92 "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" |
92 ": " ^ |
93 in |
93 Markup.markup Markup.sendback |
94 (true, st |> (if auto then |
94 ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" |
95 Proof.goal_message |
95 else "apply") ^ " " ^ s) ^ |
96 (fn () => Pretty.chunks [Pretty.str "", |
96 "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" |
97 Pretty.markup Markup.hilite |
97 in |
98 [Pretty.str message]]) |
98 (true, st |> (if auto then |
99 else |
99 Proof.goal_message |
100 tap (fn _ => Output.urgent_message message))) |
100 (fn () => Pretty.chunks [Pretty.str "", |
101 end |
101 Pretty.markup Markup.hilite |
|
102 [Pretty.str message]]) |
|
103 else |
|
104 tap (fn _ => Output.urgent_message message))) |
|
105 end |
|
106 end |
102 |
107 |
103 val invoke_try = fst oo do_try false |
108 val invoke_try = fst oo do_try false |
104 |
109 |
105 val tryN = "try" |
110 val tryN = "try" |
106 |
111 |