eliminated obsolete Proof.goal_message -- print outcome more directly;

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 03 09:25:23 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 03 14:31:15 2014 +0100
@@ -72,9 +72,9 @@
   val unregister_term_postprocessor : typ -> theory -> theory
   val pick_nits_in_term :
     Proof.state -> params -> mode -> int -> int -> int -> (term * term) list
-    -> term list -> term list -> term -> string * Proof.state
+    -> term list -> term list -> term -> string * string list
   val pick_nits_in_subgoal :
-    Proof.state -> params -> mode -> int -> int -> string * Proof.state
+    Proof.state -> params -> mode -> int -> int -> string * string list
 end;
 
 structure Nitpick : NITPICK =
@@ -234,13 +234,13 @@
          kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems,
          show_consts, evals, formats, atomss, max_potential, max_genuine,
          check_potential, check_genuine, batch_size, ...} = params
-    val state_ref = Unsynchronized.ref state
-    fun pprint print =
+    val outcome = Synchronized.var "Nitpick.outcome" (Queue.empty: string Queue.T)
+    fun pprint print prt =
       if mode = Auto_Try then
-        Unsynchronized.change state_ref o Proof.goal_message o K
-        o Pretty.mark Markup.information
+        Synchronized.change outcome
+          (Queue.enqueue (Pretty.string_of (Pretty.mark Markup.information prt)))
       else
-        print o Pretty.string_of
+        print (Pretty.string_of prt)
     val pprint_a = pprint writeln
     fun pprint_nt f = () |> is_mode_nt mode ? pprint writeln o f
     fun pprint_v f = () |> verbose ? pprint writeln o f
@@ -1007,7 +1007,7 @@
                 "Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^
                 ".")
     val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code))
-  in (outcome_code, !state_ref) end
+  in (outcome_code, Queue.content (Synchronized.value outcome)) end
 
 (* Give the inner timeout a chance. *)
 val timeout_bonus = seconds 1.0
@@ -1022,10 +1022,10 @@
       (* The "expect" argument is deliberately ignored if Kodkodi is missing so
          that the "Nitpick_Examples" can be processed on any machine. *)
       (print_nt (Pretty.string_of (plazy (K kodkodi_not_installed_message)));
-       ("no_kodkodi", state))
+       ("no_kodkodi", []))
     else
       let
-        val unknown_outcome = (unknownN, state)
+        val unknown_outcome = (unknownN, [])
         val deadline = Time.+ (Time.now (), timeout)
         val outcome as (outcome_code, _) =
           TimeLimit.timeLimit (Time.+ (timeout, timeout_bonus))
@@ -1068,7 +1068,7 @@
     val t = state |> Proof.raw_goal |> #goal |> prop_of
   in
     case Logic.count_prems t of
-      0 => (writeln "No subgoal!"; (noneN, state))
+      0 => (writeln "No subgoal!"; (noneN, []))
     | n =>
       let
         val t = Logic.goal_params t i |> fst

--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Nov 03 09:25:23 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Nov 03 14:31:15 2014 +0100
@@ -350,12 +350,12 @@
     val params as {blocking, debug, ...} =
       extract_params ctxt mode (default_raw_params thy) override_params
     fun go () =
-      (unknownN, state)
+      (unknownN, [])
       |> (if mode = Auto_Try then perhaps o try
           else if debug then fn f => fn x => f x
           else handle_exceptions ctxt)
-         (fn (_, state) => pick_nits_in_subgoal state params mode i step)
-  in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
+         (fn _ => pick_nits_in_subgoal state params mode i step)
+  in if blocking then go () else Future.fork (tap go) |> K (unknownN, []) end
   |> `(fn (outcome_code, _) => outcome_code = genuineN)
 
 fun string_for_raw_param (name, value) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 03 09:25:23 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 03 14:31:15 2014 +0100
@@ -24,7 +24,7 @@
     proof_method * proof_method list list -> (string * 'a) list * (proof_method * play_outcome)
   val string_of_factss : (string * fact list) list -> string
   val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
-    Proof.state -> bool * (string * Proof.state)
+    Proof.state -> bool * (string * string list)
 end;
 
 structure Sledgehammer : SLEDGEHAMMER =
@@ -214,10 +214,8 @@
     if mode = Auto_Try then
       let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
         (outcome_code,
-         state
-         |> outcome_code = someN
-            ? Proof.goal_message (fn () =>
-                  Pretty.mark Markup.information (Pretty.str (message ()))))
+          if outcome_code = someN then [Markup.markup Markup.information (message ())]
+          else [])
       end
     else if blocking then
       let
@@ -231,12 +229,12 @@
             outcome
             |> Async_Manager.break_into_chunks
             |> List.app writeln
-      in (outcome_code, state) end
+      in (outcome_code, []) end
     else
       (Async_Manager.thread SledgehammerN birth_time death_time
          (prover_description verbose name num_facts)
          ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);
-       (unknownN, state))
+       (unknownN, []))
   end
 
 val auto_try_max_facts_divisor = 2 (* FUDGE *)
@@ -259,7 +257,7 @@
   else
     (case subgoal_count state of
       0 =>
-      ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, state)))
+      ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, [])))
     | n =>
       let
         val _ = Proof.assert_backward state
@@ -303,7 +301,7 @@
               (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
           end
 
-        fun launch_provers state =
+        fun launch_provers () =
           let
             val factss = get_factss provers
             val problem =
@@ -313,7 +311,7 @@
             val launch = launch_prover params mode output_result only learn
           in
             if mode = Auto_Try then
-              (unknownN, state)
+              (unknownN, [])
               |> fold (fn prover => fn accum as (outcome_code, _) =>
                   if outcome_code = someN then accum else launch problem prover)
                 provers
@@ -321,12 +319,12 @@
               (learn chained;
                provers
                |> (if blocking then Par_List.map else map) (launch problem #> fst)
-               |> max_outcome_code |> rpair state)
+               |> max_outcome_code |> rpair [])
           end
       in
-        (if blocking then launch_provers state
-         else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
-        handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
+        (if blocking then launch_provers ()
+         else (Future.fork launch_provers; (unknownN, [])))
+        handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, []))
       end
       |> `(fn (outcome_code, _) => outcome_code = someN))
 

--- a/src/HOL/Tools/try0.ML	Mon Nov 03 09:25:23 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Mon Nov 03 14:31:15 2014 +0100
@@ -129,7 +129,7 @@
       ();
     (case par_map (fn f => f mode timeout_opt quad st) apply_methods of
       [] =>
-      (if mode = Normal then writeln "No proof found." else (); (false, (noneN, st)))
+      (if mode = Normal then writeln "No proof found." else (); (false, (noneN, [])))
     | xs as (name, command, _) :: _ =>
       let
         val xs = xs |> map (fn (name, _, n) => (n, name))
@@ -147,12 +147,10 @@
             [(_, ms)] => " (" ^ time_string ms ^ ")."
           | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
       in
-        (true, (name,
-           st
-           |> (if mode = Auto_Try then
-                 Proof.goal_message (fn () => Pretty.markup Markup.information [Pretty.str message])
-               else
-                 tap (fn _ => writeln message))))
+        (true,
+          (name,
+            if mode = Auto_Try then [Markup.markup Markup.information message]
+            else (writeln message; [])))
       end)
   end;
 

--- a/src/Pure/Isar/proof.ML	Mon Nov 03 09:25:23 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 03 14:31:15 2014 +0100
@@ -32,8 +32,6 @@
   val assert_no_chain: state -> state
   val enter_forward: state -> state
   val has_bottom_goal: state -> bool
-  val goal_message: (unit -> Pretty.T) -> state -> state
-  val pretty_goal_messages: state -> Pretty.T list
   val pretty_state: int -> state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.seq
   val refine_end: Method.text -> state -> state Seq.seq
@@ -151,7 +149,6 @@
   Goal of
    {statement: (string * Position.T) * term list list * term,
       (*goal kind and statement (starting with vars), initial proposition*)
-    messages: (unit -> Pretty.T) list,    (*persistent messages (hints etc.)*)
     using: thm list,                      (*goal facts*)
     goal: thm,                            (*subgoals ==> statement*)
     before_qed: Method.text option,
@@ -159,8 +156,8 @@
       (thm list list -> state -> state) *
       (thm list list -> context -> context)};
 
-fun make_goal (statement, messages, using, goal, before_qed, after_qed) =
-  Goal {statement = statement, messages = messages, using = using, goal = goal,
+fun make_goal (statement, using, goal, before_qed, after_qed) =
+  Goal {statement = statement, using = using, goal = goal,
     before_qed = before_qed, after_qed = after_qed};
 
 fun make_node (context, facts, mode, goal) =
@@ -318,8 +315,8 @@
   (case Stack.dest stack of
     (Node {context, facts, mode, goal = SOME goal}, node :: nodes) =>
       let
-        val Goal {statement, messages, using, goal, before_qed, after_qed} = goal;
-        val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed));
+        val Goal {statement, using, goal, before_qed, after_qed} = goal;
+        val goal' = make_goal (g (statement, using, goal, before_qed, after_qed));
         val node' = map_node_context h node;
         val stack' = Stack.make (make_node (f context, facts, mode, SOME goal')) (node' :: nodes);
       in State stack' end
@@ -331,14 +328,11 @@
       in State (Stack.make nd' (node' :: nodes')) end
   | _ => State stack);
 
-fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
-  (statement, [], using, goal, before_qed, after_qed)) I;
+fun provide_goal goal = map_goal I (fn (statement, using, _, before_qed, after_qed) =>
+  (statement, using, goal, before_qed, after_qed)) I;
 
-fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) =>
-  (statement, msg :: messages, using, goal, before_qed, after_qed)) I;
-
-fun using_facts using = map_goal I (fn (statement, _, _, goal, before_qed, after_qed) =>
-  (statement, [], using, goal, before_qed, after_qed)) I;
+fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) =>
+  (statement, using, goal, before_qed, after_qed)) I;
 
 local
   fun find i state =
@@ -355,11 +349,6 @@
 
 (** pretty_state **)
 
-fun pretty_goal_messages state =
-  (case try find_goal state of
-    SOME (_, (_, {messages, ...})) => map (fn msg => msg ()) (rev messages)
-  | NONE => []);
-
 fun pretty_facts _ _ NONE = []
   | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths, Pretty.str ""];
 
@@ -369,11 +358,10 @@
     val verbose = Config.get ctxt Proof_Context.verbose;
 
     fun prt_goal (SOME (_, (_,
-      {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
+      {statement = ((_, pos), _, _), using, goal, before_qed = _, after_qed = _}))) =
           pretty_facts ctxt "using"
             (if mode <> Backward orelse null using then NONE else SOME using) @
-          [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @
-          (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
+          [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal
       | prt_goal NONE = [];
 
     val prt_ctxt =
@@ -412,15 +400,14 @@
     (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
 
 fun apply_method text ctxt state =
-  #2 (#2 (find_goal state))
-  |> (fn {statement, messages = _, using, goal, before_qed, after_qed} =>
+  #2 (#2 (find_goal state)) |> (fn {statement, using, goal, before_qed, after_qed} =>
     Method.evaluate text ctxt using goal
     |> Seq.map (fn (meth_cases, goal') =>
       state
       |> map_goal
           (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
            Proof_Context.update_cases true meth_cases)
-          (K (statement, [], using, goal', before_qed, after_qed)) I));
+          (K (statement, using, goal', before_qed, after_qed)) I));
 
 in
 
@@ -716,11 +703,11 @@
     (fn ctxt => ctxt |> Proof_Context.note_thmss ""
       (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
   |> (fn (named_facts, state') =>
-    state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
+    state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) =>
       let
         val ctxt = context_of state';
         val ths = maps snd named_facts;
-      in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I);
+      in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I);
 
 fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
 fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths);
@@ -918,7 +905,7 @@
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)
-    |> set_goal (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed'))
+    |> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed'))
     |> map_context (Proof_Context.auto_bind_goal props)
     |> chaining ? (`the_facts #-> using_facts)
     |> reset_facts
@@ -1130,7 +1117,7 @@
   let
     val _ = assert_backward state;
     val (goal_ctxt, (_, goal)) = find_goal state;
-    val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal;
+    val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal;
     val goal_tfrees =
       fold Term.add_tfrees
         (prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) [];
@@ -1145,7 +1132,7 @@
     val result_ctxt =
       state
       |> map_context reset_result
-      |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
+      |> map_goal I (K (statement', using, goal', before_qed, after_qed'))
         (fold (Variable.declare_typ o TFree) goal_tfrees)
       |> fork_proof;
 
@@ -1153,7 +1140,7 @@
     val finished_goal = Goal.future_result goal_ctxt future_thm prop';
     val state' =
       state
-      |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I;
+      |> map_goal I (K (statement, using, finished_goal, NONE, after_qed)) I;
   in (Future.map fst result_ctxt, state') end;
 
 end;

--- a/src/Tools/quickcheck.ML	Mon Nov 03 09:25:23 2014 +0100
+++ b/src/Tools/quickcheck.ML	Mon Nov 03 14:31:15 2014 +0100
@@ -552,20 +552,16 @@
       |> try (test_goal (false, false) ([], []) i);
   in
     (case res of
-      NONE => (unknownN, state)
+      NONE => (unknownN, [])
     | SOME results =>
         let
           val msg = pretty_counterex ctxt auto (Option.map (the o get_first response_of) results)
         in
           if is_some results then
             (genuineN,
-             state
-             |> (if auto then
-                   Proof.goal_message (K (Pretty.mark Markup.information msg))
-                 else
-                   tap (fn _ => writeln (Pretty.string_of msg))))
-          else
-            (noneN, state)
+              if auto then [Pretty.string_of (Pretty.mark Markup.information msg)]
+              else (writeln (Pretty.string_of msg); []))
+          else (noneN, [])
         end)
   end
   |> `(fn (outcome_code, _) => outcome_code = genuineN);

--- a/src/Tools/solve_direct.ML	Mon Nov 03 09:25:23 2014 +0100
+++ b/src/Tools/solve_direct.ML	Mon Nov 03 14:31:15 2014 +0100
@@ -15,7 +15,7 @@
   val noneN: string
   val unknownN: string
   val max_solutions: int Unsynchronized.ref
-  val solve_direct: Proof.state -> bool * (string * Proof.state)
+  val solve_direct: Proof.state -> bool * (string * string list)
 end;
 
 structure Solve_Direct: SOLVE_DIRECT =
@@ -76,22 +76,17 @@
     (case try seek_against_goal () of
       SOME (SOME results) =>
         (someN,
-          state |>
-            (if mode = Auto_Try then
-               Proof.goal_message
-                 (fn () =>
-                   Pretty.markup Markup.information (message results))
-             else
-               tap (fn _ =>
-                 writeln (Pretty.string_of (Pretty.chunks (message results))))))
+          if mode = Auto_Try then
+            [Pretty.string_of (Pretty.markup Markup.information (message results))]
+          else (writeln (Pretty.string_of (Pretty.chunks (message results))); []))
     | SOME NONE =>
         (if mode = Normal then writeln "No proof found."
          else ();
-         (noneN, state))
+         (noneN, []))
     | NONE =>
         (if mode = Normal then writeln "An error occurred."
          else ();
-         (unknownN, state)))
+         (unknownN, [])))
   end
   |> `(fn (outcome_code, _) => outcome_code = someN);
 

--- 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 ()}