quiet Metis in "try"
authorblanchet
Mon Dec 06 14:47:58 2010 +0100 (2010-12-06)
changeset 410389592334001d5
parent 41018 83f241623b86
child 41039 405a9f41ad6b
quiet Metis in "try"
src/HOL/Tools/try.ML
     1.1 --- a/src/HOL/Tools/try.ML	Mon Dec 06 13:46:45 2010 +0100
     1.2 +++ b/src/HOL/Tools/try.ML	Mon Dec 06 14:47:58 2010 +0100
     1.3 @@ -77,28 +77,33 @@
     1.4  fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
     1.5  
     1.6  fun do_try auto timeout_opt st =
     1.7 -  case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
     1.8 -                  |> map_filter I |> sort (int_ord o pairself snd) of
     1.9 -    [] => (if auto then () else writeln "No proof found."; (false, st))
    1.10 -  | xs as (s, _) :: _ =>
    1.11 -    let
    1.12 -      val xs = xs |> map swap |> AList.coalesce (op =)
    1.13 -                  |> map (swap o apsnd commas)
    1.14 -      val message =
    1.15 -        (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^
    1.16 -        Markup.markup Markup.sendback
    1.17 -            ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
    1.18 -             " " ^ s) ^
    1.19 -        "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
    1.20 -    in
    1.21 -      (true, st |> (if auto then
    1.22 -                      Proof.goal_message
    1.23 -                          (fn () => Pretty.chunks [Pretty.str "",
    1.24 -                                    Pretty.markup Markup.hilite
    1.25 -                                                  [Pretty.str message]])
    1.26 -                    else
    1.27 -                      tap (fn _ => Output.urgent_message message)))
    1.28 -    end
    1.29 +  let
    1.30 +    val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
    1.31 +  in
    1.32 +    case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
    1.33 +                    |> map_filter I |> sort (int_ord o pairself snd) of
    1.34 +      [] => (if auto then () else writeln "No proof found."; (false, st))
    1.35 +    | xs as (s, _) :: _ =>
    1.36 +      let
    1.37 +        val xs = xs |> map swap |> AList.coalesce (op =)
    1.38 +                    |> map (swap o apsnd commas)
    1.39 +        val message =
    1.40 +          (if auto then "Auto Try found a proof" else "Try this command") ^
    1.41 +          ": " ^
    1.42 +          Markup.markup Markup.sendback
    1.43 +              ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
    1.44 +                else "apply") ^ " " ^ s) ^
    1.45 +          "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
    1.46 +      in
    1.47 +        (true, st |> (if auto then
    1.48 +                        Proof.goal_message
    1.49 +                            (fn () => Pretty.chunks [Pretty.str "",
    1.50 +                                      Pretty.markup Markup.hilite
    1.51 +                                                    [Pretty.str message]])
    1.52 +                      else
    1.53 +                        tap (fn _ => Output.urgent_message message)))
    1.54 +      end
    1.55 +  end
    1.56  
    1.57  val invoke_try = fst oo do_try false
    1.58