--- a/src/HOL/Tools/try.ML Mon Dec 06 13:46:45 2010 +0100
+++ b/src/HOL/Tools/try.ML Mon Dec 06 14:47:58 2010 +0100
@@ -77,28 +77,33 @@
fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
fun do_try auto timeout_opt st =
- case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
- |> map_filter I |> sort (int_ord o pairself snd) of
- [] => (if auto then () else writeln "No proof found."; (false, st))
- | xs as (s, _) :: _ =>
- let
- val xs = xs |> map swap |> AList.coalesce (op =)
- |> map (swap o apsnd commas)
- val message =
- (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^
- Markup.markup Markup.sendback
- ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
- " " ^ s) ^
- "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
- in
- (true, st |> (if auto then
- Proof.goal_message
- (fn () => Pretty.chunks [Pretty.str "",
- Pretty.markup Markup.hilite
- [Pretty.str message]])
- else
- tap (fn _ => Output.urgent_message message)))
- end
+ let
+ val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
+ in
+ case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
+ |> map_filter I |> sort (int_ord o pairself snd) of
+ [] => (if auto then () else writeln "No proof found."; (false, st))
+ | xs as (s, _) :: _ =>
+ let
+ val xs = xs |> map swap |> AList.coalesce (op =)
+ |> map (swap o apsnd commas)
+ val message =
+ (if auto then "Auto Try found a proof" else "Try this command") ^
+ ": " ^
+ Markup.markup Markup.sendback
+ ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
+ else "apply") ^ " " ^ s) ^
+ "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
+ in
+ (true, st |> (if auto then
+ Proof.goal_message
+ (fn () => Pretty.chunks [Pretty.str "",
+ Pretty.markup Markup.hilite
+ [Pretty.str message]])
+ else
+ tap (fn _ => Output.urgent_message message)))
+ end
+ end
val invoke_try = fst oo do_try false