src/Pure/Isar/proof.ML

   val assert_forward_or_chain: state -> state
   val assert_backward: state -> state
   val assert_no_chain: state -> state
   val enter_forward: state -> state
   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
   val refine_insert: thm list -> state -> state
   val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq

 
 
 
 (** 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 ""];
 
 fun pretty_state nr state =
   let