# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID 5a0dec7bc099be4b4e53120da1d4ccac1efafbfa
# Parent  58150aa44941616ac3bf34134dc94be4c3aacb91
handle non-auto try case gracefully in Solve Direct

diff -r 58150aa44941 -r 5a0dec7bc099 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
@@ -16,13 +16,15 @@
   val unknownN: string
   val auto: bool Unsynchronized.ref
   val max_solutions: int Unsynchronized.ref
-  val solve_direct: bool -> Proof.state -> bool * (string * Proof.state)
+  val solve_direct: Proof.state -> bool * (string * Proof.state)
   val setup: theory -> theory
 end;
 
 structure Solve_Direct: SOLVE_DIRECT =
 struct
 
+datatype mode = Auto_Try | Try | Normal
+
 val solve_directN = "solve_direct";
 
 val someN = "some";
@@ -44,7 +46,7 @@
 
 (* solve_direct command *)
 
-fun solve_direct auto state =
+fun do_solve_direct mode state =
   let
     val ctxt = Proof.context_of state;
 
@@ -55,7 +57,7 @@
     fun prt_result (goal, results) =
       let
         val msg =
-          (if auto then "Auto " else "") ^ solve_directN ^ ": " ^
+          (if mode = Auto_Try then "Auto " else "") ^ solve_directN ^ ": " ^
           (case goal of
             NONE => "The current goal"
           | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
@@ -83,29 +85,38 @@
       SOME (SOME results) =>
         (someN,
           state |>
-           (if auto then
-             Proof.goal_message
-               (fn () =>
-                 Pretty.chunks
-                  [Pretty.str "",
-                   Pretty.markup Markup.hilite (message results)])
-            else
-              tap (fn _ =>
-                Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
-    | SOME NONE => (noneN, state)
-    | NONE => (unknownN, state))
+            (if mode = Auto_Try then
+               Proof.goal_message
+                 (fn () =>
+                   Pretty.chunks
+                    [Pretty.str "", Pretty.markup Markup.hilite (message results)])
+             else
+               tap (fn _ =>
+                 Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
+    | SOME NONE =>
+        (if mode = Normal then Output.urgent_message "No proof found."
+         else ();
+         (noneN, state))
+    | NONE =>
+        (if mode = Normal then Output.urgent_message "An error occurred."
+         else ();
+         (unknownN, state)))
   end
   |> `(fn (outcome_code, _) => outcome_code = someN);
 
+val solve_direct = do_solve_direct Normal
+
 val _ =
   Outer_Syntax.improper_command solve_directN
     "try to solve conjectures directly with existing theorems" Keyword.diag
     (Scan.succeed
-      (Toplevel.keep (fn state => ignore (solve_direct false (Toplevel.proof_of state)))));
+      (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
 
 
 (* hook *)
 
-val setup = Try.register_tool (solve_directN, (10, auto, solve_direct));
+fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
+
+val setup = Try.register_tool (solve_directN, (10, auto, try_solve_direct));
 
 end;