1.1 --- a/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4  structure Try_Methods : TRY_METHODS =
     1.5  struct
     1.6  
     1.7 +datatype mode = Auto_Try | Try | Normal
     1.8 +
     1.9  val try_methodsN = "try_methods"
    1.10  
    1.11  val noneN = "none"
    1.12 @@ -71,9 +73,9 @@
    1.13  fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
    1.14    "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
    1.15  
    1.16 -fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
    1.17 -                    quad st =
    1.18 -  if not auto orelse run_if_auto then
    1.19 +fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode
    1.20 +                    timeout_opt quad st =
    1.21 +  if mode <> Auto_Try orelse run_if_auto_try then
    1.22      let val attrs = attrs_text attrs quad in
    1.23        do_generic timeout_opt
    1.24                   (name ^ (if all_goals andalso
    1.25 @@ -94,7 +96,7 @@
    1.26  val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
    1.27  val no_attrs = (NONE, NONE, NONE, NONE)
    1.28  
    1.29 -(* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *)
    1.30 +(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
    1.31  val named_methods =
    1.32    [("simp", ((false, true), simp_attrs)),
    1.33     ("auto", ((true, true), full_attrs)),
    1.34 @@ -109,14 +111,21 @@
    1.35  
    1.36  fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
    1.37  
    1.38 -fun do_try_methods auto timeout_opt quad st =
    1.39 +fun do_try_methods mode timeout_opt quad st =
    1.40    let
    1.41      val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
    1.42    in
    1.43 -    case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)
    1.44 +    if mode = Normal then
    1.45 +      "Trying " ^ space_implode " " (Try.serial_commas "and"
    1.46 +                                      (map (quote o fst) named_methods)) ^ "..."
    1.47 +      |> Output.urgent_message
    1.48 +    else
    1.49 +      ();
    1.50 +    case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st)
    1.51                      |> map_filter I |> sort (int_ord o pairself snd) of
    1.52 -      [] => (if auto then () else writeln "No proof found.";
    1.53 -             (false, (noneN, st)))
    1.54 +      [] =>
    1.55 +      (if mode = Normal then Output.urgent_message "No proof found." else ();
    1.56 +       (false, (noneN, st)))
    1.57      | xs as (s, _) :: _ =>
    1.58        let
    1.59          val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
    1.60 @@ -124,14 +133,16 @@
    1.61                      |> map (swap o apsnd commas)
    1.62          val need_parens = exists_string (curry (op =) " ") s
    1.63          val message =
    1.64 -          (if auto then "Auto Try Methods found a proof"
    1.65 -           else "Try this command") ^ ": " ^
    1.66 +          (case mode of
    1.67 +             Auto_Try => "Auto Try Methods found a proof"
    1.68 +           | Try => "Try Methods found a proof"
    1.69 +           | Normal => "Try this command") ^ ": " ^
    1.70            Markup.markup Markup.sendback
    1.71                ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
    1.72                  else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
    1.73            "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
    1.74        in
    1.75 -        (true, (s, st |> (if auto then
    1.76 +        (true, (s, st |> (if mode = Auto_Try then
    1.77                              Proof.goal_message
    1.78                                  (fn () => Pretty.chunks [Pretty.str "",
    1.79                                            Pretty.markup Markup.hilite
    1.80 @@ -141,10 +152,10 @@
    1.81        end
    1.82    end
    1.83  
    1.84 -fun try_methods timeout_opt = fst oo do_try_methods false timeout_opt
    1.85 +fun try_methods timeout_opt = fst oo do_try_methods Normal timeout_opt
    1.86  
    1.87  fun try_methods_trans quad =
    1.88 -  Toplevel.keep (K () o do_try_methods false (SOME default_timeout) quad
    1.89 +  Toplevel.keep (K () o do_try_methods Normal (SOME default_timeout) quad
    1.90                   o Toplevel.proof_of)
    1.91  
    1.92  fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
    1.93 @@ -180,8 +191,9 @@
    1.94        "try a combination of proof methods" Keyword.diag
    1.95        parse_try_methods_command
    1.96  
    1.97 -fun try_try_methods auto = do_try_methods auto NONE ([], [], [], [])
    1.98 +fun try_try_methods auto =
    1.99 +  do_try_methods (if auto then Auto_Try else Try) NONE ([], [], [], [])
   1.100  
   1.101 -val setup = Try.register_tool (try_methodsN, (20, auto, try_try_methods))
   1.102 +val setup = Try.register_tool (try_methodsN, (30, auto, try_try_methods))
   1.103  
   1.104  end;