eliminated obsolete Proof.goal_message -- print outcome more directly;
authorwenzelm
Mon Nov 03 14:31:15 2014 +0100 (2014-11-03 ago)
changeset 5889220aa19ecf2cc
parent 58891 81a1295c69ad
child 58893 9e0ecb66d6a7
eliminated obsolete Proof.goal_message -- print outcome more directly;
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/try0.ML
src/Pure/Isar/proof.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 03 09:25:23 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 03 14:31:15 2014 +0100
     1.3 @@ -72,9 +72,9 @@
     1.4    val unregister_term_postprocessor : typ -> theory -> theory
     1.5    val pick_nits_in_term :
     1.6      Proof.state -> params -> mode -> int -> int -> int -> (term * term) list
     1.7 -    -> term list -> term list -> term -> string * Proof.state
     1.8 +    -> term list -> term list -> term -> string * string list
     1.9    val pick_nits_in_subgoal :
    1.10 -    Proof.state -> params -> mode -> int -> int -> string * Proof.state
    1.11 +    Proof.state -> params -> mode -> int -> int -> string * string list
    1.12  end;
    1.13  
    1.14  structure Nitpick : NITPICK =
    1.15 @@ -234,13 +234,13 @@
    1.16           kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems,
    1.17           show_consts, evals, formats, atomss, max_potential, max_genuine,
    1.18           check_potential, check_genuine, batch_size, ...} = params
    1.19 -    val state_ref = Unsynchronized.ref state
    1.20 -    fun pprint print =
    1.21 +    val outcome = Synchronized.var "Nitpick.outcome" (Queue.empty: string Queue.T)
    1.22 +    fun pprint print prt =
    1.23        if mode = Auto_Try then
    1.24 -        Unsynchronized.change state_ref o Proof.goal_message o K
    1.25 -        o Pretty.mark Markup.information
    1.26 +        Synchronized.change outcome
    1.27 +          (Queue.enqueue (Pretty.string_of (Pretty.mark Markup.information prt)))
    1.28        else
    1.29 -        print o Pretty.string_of
    1.30 +        print (Pretty.string_of prt)
    1.31      val pprint_a = pprint writeln
    1.32      fun pprint_nt f = () |> is_mode_nt mode ? pprint writeln o f
    1.33      fun pprint_v f = () |> verbose ? pprint writeln o f
    1.34 @@ -1007,7 +1007,7 @@
    1.35                  "Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^
    1.36                  ".")
    1.37      val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code))
    1.38 -  in (outcome_code, !state_ref) end
    1.39 +  in (outcome_code, Queue.content (Synchronized.value outcome)) end
    1.40  
    1.41  (* Give the inner timeout a chance. *)
    1.42  val timeout_bonus = seconds 1.0
    1.43 @@ -1022,10 +1022,10 @@
    1.44        (* The "expect" argument is deliberately ignored if Kodkodi is missing so
    1.45           that the "Nitpick_Examples" can be processed on any machine. *)
    1.46        (print_nt (Pretty.string_of (plazy (K kodkodi_not_installed_message)));
    1.47 -       ("no_kodkodi", state))
    1.48 +       ("no_kodkodi", []))
    1.49      else
    1.50        let
    1.51 -        val unknown_outcome = (unknownN, state)
    1.52 +        val unknown_outcome = (unknownN, [])
    1.53          val deadline = Time.+ (Time.now (), timeout)
    1.54          val outcome as (outcome_code, _) =
    1.55            TimeLimit.timeLimit (Time.+ (timeout, timeout_bonus))
    1.56 @@ -1068,7 +1068,7 @@
    1.57      val t = state |> Proof.raw_goal |> #goal |> prop_of
    1.58    in
    1.59      case Logic.count_prems t of
    1.60 -      0 => (writeln "No subgoal!"; (noneN, state))
    1.61 +      0 => (writeln "No subgoal!"; (noneN, []))
    1.62      | n =>
    1.63        let
    1.64          val t = Logic.goal_params t i |> fst
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Nov 03 09:25:23 2014 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Nov 03 14:31:15 2014 +0100
     2.3 @@ -350,12 +350,12 @@
     2.4      val params as {blocking, debug, ...} =
     2.5        extract_params ctxt mode (default_raw_params thy) override_params
     2.6      fun go () =
     2.7 -      (unknownN, state)
     2.8 +      (unknownN, [])
     2.9        |> (if mode = Auto_Try then perhaps o try
    2.10            else if debug then fn f => fn x => f x
    2.11            else handle_exceptions ctxt)
    2.12 -         (fn (_, state) => pick_nits_in_subgoal state params mode i step)
    2.13 -  in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
    2.14 +         (fn _ => pick_nits_in_subgoal state params mode i step)
    2.15 +  in if blocking then go () else Future.fork (tap go) |> K (unknownN, []) end
    2.16    |> `(fn (outcome_code, _) => outcome_code = genuineN)
    2.17  
    2.18  fun string_for_raw_param (name, value) =
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 03 09:25:23 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 03 14:31:15 2014 +0100
     3.3 @@ -24,7 +24,7 @@
     3.4      proof_method * proof_method list list -> (string * 'a) list * (proof_method * play_outcome)
     3.5    val string_of_factss : (string * fact list) list -> string
     3.6    val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
     3.7 -    Proof.state -> bool * (string * Proof.state)
     3.8 +    Proof.state -> bool * (string * string list)
     3.9  end;
    3.10  
    3.11  structure Sledgehammer : SLEDGEHAMMER =
    3.12 @@ -214,10 +214,8 @@
    3.13      if mode = Auto_Try then
    3.14        let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
    3.15          (outcome_code,
    3.16 -         state
    3.17 -         |> outcome_code = someN
    3.18 -            ? Proof.goal_message (fn () =>
    3.19 -                  Pretty.mark Markup.information (Pretty.str (message ()))))
    3.20 +          if outcome_code = someN then [Markup.markup Markup.information (message ())]
    3.21 +          else [])
    3.22        end
    3.23      else if blocking then
    3.24        let
    3.25 @@ -231,12 +229,12 @@
    3.26              outcome
    3.27              |> Async_Manager.break_into_chunks
    3.28              |> List.app writeln
    3.29 -      in (outcome_code, state) end
    3.30 +      in (outcome_code, []) end
    3.31      else
    3.32        (Async_Manager.thread SledgehammerN birth_time death_time
    3.33           (prover_description verbose name num_facts)
    3.34           ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);
    3.35 -       (unknownN, state))
    3.36 +       (unknownN, []))
    3.37    end
    3.38  
    3.39  val auto_try_max_facts_divisor = 2 (* FUDGE *)
    3.40 @@ -259,7 +257,7 @@
    3.41    else
    3.42      (case subgoal_count state of
    3.43        0 =>
    3.44 -      ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, state)))
    3.45 +      ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, [])))
    3.46      | n =>
    3.47        let
    3.48          val _ = Proof.assert_backward state
    3.49 @@ -303,7 +301,7 @@
    3.50                (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
    3.51            end
    3.52  
    3.53 -        fun launch_provers state =
    3.54 +        fun launch_provers () =
    3.55            let
    3.56              val factss = get_factss provers
    3.57              val problem =
    3.58 @@ -313,7 +311,7 @@
    3.59              val launch = launch_prover params mode output_result only learn
    3.60            in
    3.61              if mode = Auto_Try then
    3.62 -              (unknownN, state)
    3.63 +              (unknownN, [])
    3.64                |> fold (fn prover => fn accum as (outcome_code, _) =>
    3.65                    if outcome_code = someN then accum else launch problem prover)
    3.66                  provers
    3.67 @@ -321,12 +319,12 @@
    3.68                (learn chained;
    3.69                 provers
    3.70                 |> (if blocking then Par_List.map else map) (launch problem #> fst)
    3.71 -               |> max_outcome_code |> rpair state)
    3.72 +               |> max_outcome_code |> rpair [])
    3.73            end
    3.74        in
    3.75 -        (if blocking then launch_provers state
    3.76 -         else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
    3.77 -        handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
    3.78 +        (if blocking then launch_provers ()
    3.79 +         else (Future.fork launch_provers; (unknownN, [])))
    3.80 +        handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, []))
    3.81        end
    3.82        |> `(fn (outcome_code, _) => outcome_code = someN))
    3.83  
     4.1 --- a/src/HOL/Tools/try0.ML	Mon Nov 03 09:25:23 2014 +0100
     4.2 +++ b/src/HOL/Tools/try0.ML	Mon Nov 03 14:31:15 2014 +0100
     4.3 @@ -129,7 +129,7 @@
     4.4        ();
     4.5      (case par_map (fn f => f mode timeout_opt quad st) apply_methods of
     4.6        [] =>
     4.7 -      (if mode = Normal then writeln "No proof found." else (); (false, (noneN, st)))
     4.8 +      (if mode = Normal then writeln "No proof found." else (); (false, (noneN, [])))
     4.9      | xs as (name, command, _) :: _ =>
    4.10        let
    4.11          val xs = xs |> map (fn (name, _, n) => (n, name))
    4.12 @@ -147,12 +147,10 @@
    4.13              [(_, ms)] => " (" ^ time_string ms ^ ")."
    4.14            | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
    4.15        in
    4.16 -        (true, (name,
    4.17 -           st
    4.18 -           |> (if mode = Auto_Try then
    4.19 -                 Proof.goal_message (fn () => Pretty.markup Markup.information [Pretty.str message])
    4.20 -               else
    4.21 -                 tap (fn _ => writeln message))))
    4.22 +        (true,
    4.23 +          (name,
    4.24 +            if mode = Auto_Try then [Markup.markup Markup.information message]
    4.25 +            else (writeln message; [])))
    4.26        end)
    4.27    end;
    4.28  
     5.1 --- a/src/Pure/Isar/proof.ML	Mon Nov 03 09:25:23 2014 +0100
     5.2 +++ b/src/Pure/Isar/proof.ML	Mon Nov 03 14:31:15 2014 +0100
     5.3 @@ -32,8 +32,6 @@
     5.4    val assert_no_chain: state -> state
     5.5    val enter_forward: state -> state
     5.6    val has_bottom_goal: state -> bool
     5.7 -  val goal_message: (unit -> Pretty.T) -> state -> state
     5.8 -  val pretty_goal_messages: state -> Pretty.T list
     5.9    val pretty_state: int -> state -> Pretty.T list
    5.10    val refine: Method.text -> state -> state Seq.seq
    5.11    val refine_end: Method.text -> state -> state Seq.seq
    5.12 @@ -151,7 +149,6 @@
    5.13    Goal of
    5.14     {statement: (string * Position.T) * term list list * term,
    5.15        (*goal kind and statement (starting with vars), initial proposition*)
    5.16 -    messages: (unit -> Pretty.T) list,    (*persistent messages (hints etc.)*)
    5.17      using: thm list,                      (*goal facts*)
    5.18      goal: thm,                            (*subgoals ==> statement*)
    5.19      before_qed: Method.text option,
    5.20 @@ -159,8 +156,8 @@
    5.21        (thm list list -> state -> state) *
    5.22        (thm list list -> context -> context)};
    5.23  
    5.24 -fun make_goal (statement, messages, using, goal, before_qed, after_qed) =
    5.25 -  Goal {statement = statement, messages = messages, using = using, goal = goal,
    5.26 +fun make_goal (statement, using, goal, before_qed, after_qed) =
    5.27 +  Goal {statement = statement, using = using, goal = goal,
    5.28      before_qed = before_qed, after_qed = after_qed};
    5.29  
    5.30  fun make_node (context, facts, mode, goal) =
    5.31 @@ -318,8 +315,8 @@
    5.32    (case Stack.dest stack of
    5.33      (Node {context, facts, mode, goal = SOME goal}, node :: nodes) =>
    5.34        let
    5.35 -        val Goal {statement, messages, using, goal, before_qed, after_qed} = goal;
    5.36 -        val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed));
    5.37 +        val Goal {statement, using, goal, before_qed, after_qed} = goal;
    5.38 +        val goal' = make_goal (g (statement, using, goal, before_qed, after_qed));
    5.39          val node' = map_node_context h node;
    5.40          val stack' = Stack.make (make_node (f context, facts, mode, SOME goal')) (node' :: nodes);
    5.41        in State stack' end
    5.42 @@ -331,14 +328,11 @@
    5.43        in State (Stack.make nd' (node' :: nodes')) end
    5.44    | _ => State stack);
    5.45  
    5.46 -fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
    5.47 -  (statement, [], using, goal, before_qed, after_qed)) I;
    5.48 +fun provide_goal goal = map_goal I (fn (statement, using, _, before_qed, after_qed) =>
    5.49 +  (statement, using, goal, before_qed, after_qed)) I;
    5.50  
    5.51 -fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) =>
    5.52 -  (statement, msg :: messages, using, goal, before_qed, after_qed)) I;
    5.53 -
    5.54 -fun using_facts using = map_goal I (fn (statement, _, _, goal, before_qed, after_qed) =>
    5.55 -  (statement, [], using, goal, before_qed, after_qed)) I;
    5.56 +fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) =>
    5.57 +  (statement, using, goal, before_qed, after_qed)) I;
    5.58  
    5.59  local
    5.60    fun find i state =
    5.61 @@ -355,11 +349,6 @@
    5.62  
    5.63  (** pretty_state **)
    5.64  
    5.65 -fun pretty_goal_messages state =
    5.66 -  (case try find_goal state of
    5.67 -    SOME (_, (_, {messages, ...})) => map (fn msg => msg ()) (rev messages)
    5.68 -  | NONE => []);
    5.69 -
    5.70  fun pretty_facts _ _ NONE = []
    5.71    | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths, Pretty.str ""];
    5.72  
    5.73 @@ -369,11 +358,10 @@
    5.74      val verbose = Config.get ctxt Proof_Context.verbose;
    5.75  
    5.76      fun prt_goal (SOME (_, (_,
    5.77 -      {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
    5.78 +      {statement = ((_, pos), _, _), using, goal, before_qed = _, after_qed = _}))) =
    5.79            pretty_facts ctxt "using"
    5.80              (if mode <> Backward orelse null using then NONE else SOME using) @
    5.81 -          [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @
    5.82 -          (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
    5.83 +          [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal
    5.84        | prt_goal NONE = [];
    5.85  
    5.86      val prt_ctxt =
    5.87 @@ -412,15 +400,14 @@
    5.88      (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
    5.89  
    5.90  fun apply_method text ctxt state =
    5.91 -  #2 (#2 (find_goal state))
    5.92 -  |> (fn {statement, messages = _, using, goal, before_qed, after_qed} =>
    5.93 +  #2 (#2 (find_goal state)) |> (fn {statement, using, goal, before_qed, after_qed} =>
    5.94      Method.evaluate text ctxt using goal
    5.95      |> Seq.map (fn (meth_cases, goal') =>
    5.96        state
    5.97        |> map_goal
    5.98            (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
    5.99             Proof_Context.update_cases true meth_cases)
   5.100 -          (K (statement, [], using, goal', before_qed, after_qed)) I));
   5.101 +          (K (statement, using, goal', before_qed, after_qed)) I));
   5.102  
   5.103  in
   5.104  
   5.105 @@ -716,11 +703,11 @@
   5.106      (fn ctxt => ctxt |> Proof_Context.note_thmss ""
   5.107        (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
   5.108    |> (fn (named_facts, state') =>
   5.109 -    state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
   5.110 +    state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) =>
   5.111        let
   5.112          val ctxt = context_of state';
   5.113          val ths = maps snd named_facts;
   5.114 -      in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I);
   5.115 +      in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I);
   5.116  
   5.117  fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
   5.118  fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths);
   5.119 @@ -918,7 +905,7 @@
   5.120    in
   5.121      goal_state
   5.122      |> map_context (init_context #> Variable.set_body true)
   5.123 -    |> set_goal (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed'))
   5.124 +    |> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed'))
   5.125      |> map_context (Proof_Context.auto_bind_goal props)
   5.126      |> chaining ? (`the_facts #-> using_facts)
   5.127      |> reset_facts
   5.128 @@ -1130,7 +1117,7 @@
   5.129    let
   5.130      val _ = assert_backward state;
   5.131      val (goal_ctxt, (_, goal)) = find_goal state;
   5.132 -    val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal;
   5.133 +    val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal;
   5.134      val goal_tfrees =
   5.135        fold Term.add_tfrees
   5.136          (prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) [];
   5.137 @@ -1145,7 +1132,7 @@
   5.138      val result_ctxt =
   5.139        state
   5.140        |> map_context reset_result
   5.141 -      |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
   5.142 +      |> map_goal I (K (statement', using, goal', before_qed, after_qed'))
   5.143          (fold (Variable.declare_typ o TFree) goal_tfrees)
   5.144        |> fork_proof;
   5.145  
   5.146 @@ -1153,7 +1140,7 @@
   5.147      val finished_goal = Goal.future_result goal_ctxt future_thm prop';
   5.148      val state' =
   5.149        state
   5.150 -      |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I;
   5.151 +      |> map_goal I (K (statement, using, finished_goal, NONE, after_qed)) I;
   5.152    in (Future.map fst result_ctxt, state') end;
   5.153  
   5.154  end;
     6.1 --- a/src/Tools/quickcheck.ML	Mon Nov 03 09:25:23 2014 +0100
     6.2 +++ b/src/Tools/quickcheck.ML	Mon Nov 03 14:31:15 2014 +0100
     6.3 @@ -552,20 +552,16 @@
     6.4        |> try (test_goal (false, false) ([], []) i);
     6.5    in
     6.6      (case res of
     6.7 -      NONE => (unknownN, state)
     6.8 +      NONE => (unknownN, [])
     6.9      | SOME results =>
    6.10          let
    6.11            val msg = pretty_counterex ctxt auto (Option.map (the o get_first response_of) results)
    6.12          in
    6.13            if is_some results then
    6.14              (genuineN,
    6.15 -             state
    6.16 -             |> (if auto then
    6.17 -                   Proof.goal_message (K (Pretty.mark Markup.information msg))
    6.18 -                 else
    6.19 -                   tap (fn _ => writeln (Pretty.string_of msg))))
    6.20 -          else
    6.21 -            (noneN, state)
    6.22 +              if auto then [Pretty.string_of (Pretty.mark Markup.information msg)]
    6.23 +              else (writeln (Pretty.string_of msg); []))
    6.24 +          else (noneN, [])
    6.25          end)
    6.26    end
    6.27    |> `(fn (outcome_code, _) => outcome_code = genuineN);
     7.1 --- a/src/Tools/solve_direct.ML	Mon Nov 03 09:25:23 2014 +0100
     7.2 +++ b/src/Tools/solve_direct.ML	Mon Nov 03 14:31:15 2014 +0100
     7.3 @@ -15,7 +15,7 @@
     7.4    val noneN: string
     7.5    val unknownN: string
     7.6    val max_solutions: int Unsynchronized.ref
     7.7 -  val solve_direct: Proof.state -> bool * (string * Proof.state)
     7.8 +  val solve_direct: Proof.state -> bool * (string * string list)
     7.9  end;
    7.10  
    7.11  structure Solve_Direct: SOLVE_DIRECT =
    7.12 @@ -76,22 +76,17 @@
    7.13      (case try seek_against_goal () of
    7.14        SOME (SOME results) =>
    7.15          (someN,
    7.16 -          state |>
    7.17 -            (if mode = Auto_Try then
    7.18 -               Proof.goal_message
    7.19 -                 (fn () =>
    7.20 -                   Pretty.markup Markup.information (message results))
    7.21 -             else
    7.22 -               tap (fn _ =>
    7.23 -                 writeln (Pretty.string_of (Pretty.chunks (message results))))))
    7.24 +          if mode = Auto_Try then
    7.25 +            [Pretty.string_of (Pretty.markup Markup.information (message results))]
    7.26 +          else (writeln (Pretty.string_of (Pretty.chunks (message results))); []))
    7.27      | SOME NONE =>
    7.28          (if mode = Normal then writeln "No proof found."
    7.29           else ();
    7.30 -         (noneN, state))
    7.31 +         (noneN, []))
    7.32      | NONE =>
    7.33          (if mode = Normal then writeln "An error occurred."
    7.34           else ();
    7.35 -         (unknownN, state)))
    7.36 +         (unknownN, [])))
    7.37    end
    7.38    |> `(fn (outcome_code, _) => outcome_code = someN);
    7.39  
     8.1 --- a/src/Tools/try.ML	Mon Nov 03 09:25:23 2014 +0100
     8.2 +++ b/src/Tools/try.ML	Mon Nov 03 14:31:15 2014 +0100
     8.3 @@ -7,7 +7,7 @@
     8.4  signature TRY =
     8.5  sig
     8.6    type tool =
     8.7 -    string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
     8.8 +    string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
     8.9  
    8.10    val tryN : string
    8.11  
    8.12 @@ -22,7 +22,7 @@
    8.13  struct
    8.14  
    8.15  type tool =
    8.16 -  string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
    8.17 +  string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
    8.18  
    8.19  val tryN = "try"
    8.20  
    8.21 @@ -87,9 +87,9 @@
    8.22    |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
    8.23    |> Par_List.get_some (fn tool =>
    8.24                             case try (tool true) state of
    8.25 -                             SOME (true, (_, state)) => SOME state
    8.26 +                             SOME (true, (_, outcome)) => SOME outcome
    8.27                             | _ => NONE)
    8.28 -  |> the_default state
    8.29 +  |> the_default []
    8.30  
    8.31  
    8.32  (* asynchronous print function (PIDE) *)
    8.33 @@ -111,8 +111,7 @@
    8.34              in
    8.35                if auto_time_limit > 0.0 then
    8.36                  (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
    8.37 -                  (true, (_, state')) =>
    8.38 -                    List.app Pretty.writeln (Proof.pretty_goal_messages state')
    8.39 +                  (true, (_, outcome)) => List.app writeln outcome
    8.40                  | _ => ())
    8.41                else ()
    8.42              end handle exn => if Exn.is_interrupt exn then reraise exn else ()}