src/Tools/try.ML

 *)
 
 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
 
   val serial_commas : string -> string list -> string list
   val subgoal_count : Proof.state -> int

 
 structure Try : TRY =
 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"
 
 
 (* helpers *)

 fun auto_try state =
   get_tools (Proof.theory_of state)
   |> 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) *)
 
 fun print_function ((name, (weight, auto, tool)): tool) =

                 |> Proof.map_context (Context_Position.set_visible false)
               val auto_time_limit = Options.default_real @{system_option auto_time_limit}
             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 ()}
       else NONE)