# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID 0f15575a6465f27b6e9f53b9ec734219e05b176e
# Parent  5a0dec7bc099be4b4e53120da1d4ccac1efafbfa
handle non-auto try cases gracefully in Try Methods

diff -r 5a0dec7bc099 -r 0f15575a6465 src/HOL/Tools/try_methods.ML
--- a/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
@@ -18,6 +18,8 @@
 structure Try_Methods : TRY_METHODS =
 struct
 
+datatype mode = Auto_Try | Try | Normal
+
 val try_methodsN = "try_methods"
 
 val noneN = "none"
@@ -71,9 +73,9 @@
 fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
   "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
 
-fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
-                    quad st =
-  if not auto orelse run_if_auto then
+fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode
+                    timeout_opt quad st =
+  if mode <> Auto_Try orelse run_if_auto_try then
     let val attrs = attrs_text attrs quad in
       do_generic timeout_opt
                  (name ^ (if all_goals andalso
@@ -94,7 +96,7 @@
 val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
 val no_attrs = (NONE, NONE, NONE, NONE)
 
-(* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *)
+(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
 val named_methods =
   [("simp", ((false, true), simp_attrs)),
    ("auto", ((true, true), full_attrs)),
@@ -109,14 +111,21 @@
 
 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
 
-fun do_try_methods auto timeout_opt quad st =
+fun do_try_methods mode timeout_opt quad st =
   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 quad st)
+    if mode = Normal then
+      "Trying " ^ space_implode " " (Try.serial_commas "and"
+                                      (map (quote o fst) named_methods)) ^ "..."
+      |> Output.urgent_message
+    else
+      ();
+    case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st)
                     |> map_filter I |> sort (int_ord o pairself snd) of
-      [] => (if auto then () else writeln "No proof found.";
-             (false, (noneN, st)))
+      [] =>
+      (if mode = Normal then Output.urgent_message "No proof found." else ();
+       (false, (noneN, st)))
     | xs as (s, _) :: _ =>
       let
         val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
@@ -124,14 +133,16 @@
                     |> map (swap o apsnd commas)
         val need_parens = exists_string (curry (op =) " ") s
         val message =
-          (if auto then "Auto Try Methods found a proof"
-           else "Try this command") ^ ": " ^
+          (case mode of
+             Auto_Try => "Auto Try Methods found a proof"
+           | Try => "Try Methods found a proof"
+           | Normal => "Try this command") ^ ": " ^
           Markup.markup Markup.sendback
               ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
                 else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
           "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
       in
-        (true, (s, st |> (if auto then
+        (true, (s, st |> (if mode = Auto_Try then
                             Proof.goal_message
                                 (fn () => Pretty.chunks [Pretty.str "",
                                           Pretty.markup Markup.hilite
@@ -141,10 +152,10 @@
       end
   end
 
-fun try_methods timeout_opt = fst oo do_try_methods false timeout_opt
+fun try_methods timeout_opt = fst oo do_try_methods Normal timeout_opt
 
 fun try_methods_trans quad =
-  Toplevel.keep (K () o do_try_methods false (SOME default_timeout) quad
+  Toplevel.keep (K () o do_try_methods Normal (SOME default_timeout) quad
                  o Toplevel.proof_of)
 
 fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
@@ -180,8 +191,9 @@
       "try a combination of proof methods" Keyword.diag
       parse_try_methods_command
 
-fun try_try_methods auto = do_try_methods auto NONE ([], [], [], [])
+fun try_try_methods auto =
+  do_try_methods (if auto then Auto_Try else Try) NONE ([], [], [], [])
 
-val setup = Try.register_tool (try_methodsN, (20, auto, try_try_methods))
+val setup = Try.register_tool (try_methodsN, (30, auto, try_try_methods))
 
 end;