src/Tools/try.ML

--- a/src/Tools/try.ML	Mon Nov 03 09:25:23 2014 +0100
+++ b/src/Tools/try.ML	Mon Nov 03 14:31:15 2014 +0100
@@ -7,7 +7,7 @@
 signature TRY =
 sig
   type tool =
-    string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
+    string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
 
   val tryN : string
 
@@ -22,7 +22,7 @@
 struct
 
 type tool =
-  string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
+  string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
 
 val tryN = "try"
 
@@ -87,9 +87,9 @@
   |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
   |> Par_List.get_some (fn tool =>
                            case try (tool true) state of
-                             SOME (true, (_, state)) => SOME state
+                             SOME (true, (_, outcome)) => SOME outcome
                            | _ => NONE)
-  |> the_default state
+  |> the_default []
 
 
 (* asynchronous print function (PIDE) *)
@@ -111,8 +111,7 @@
             in
               if auto_time_limit > 0.0 then
                 (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
-                  (true, (_, state')) =>
-                    List.app Pretty.writeln (Proof.pretty_goal_messages state')
+                  (true, (_, outcome)) => List.app writeln outcome
                 | _ => ())
               else ()
             end handle exn => if Exn.is_interrupt exn then reraise exn else ()}