reports with body text, not just markup;

--- a/src/Pure/General/position.ML	Sat Aug 11 15:54:18 2012 +0200
+++ b/src/Pure/General/position.ML	Sat Aug 11 17:23:09 2012 +0200
@@ -37,6 +37,8 @@
   val report_text: T -> Markup.T -> string -> unit
   val report: T -> Markup.T -> unit
   type report = T * Markup.T
+  type report_text = report * string
+  val reports_text: report_text list -> unit
   val reports: report list -> unit
   val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
   val str_of: T -> string
@@ -164,11 +166,14 @@
 fun report pos markup = report_text pos markup "";
 
 type report = T * Markup.T;
+type report_text = report * string;
 
-val reports =
-  map (fn (pos, m) => if is_reported pos then Markup.markup_only (markup pos m) else "")
+val reports_text =
+  map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
   #> implode #> Output.report;
 
+val reports = map (rpair "") #> reports_text;
+
 fun store_reports _ [] _ _ = ()
   | store_reports (r: report list Unsynchronized.ref) ps markup x =
       let val ms = markup x

--- a/src/Pure/context_position.ML	Sat Aug 11 15:54:18 2012 +0200
+++ b/src/Pure/context_position.ML	Sat Aug 11 17:23:09 2012 +0200
@@ -16,6 +16,7 @@
   val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
   val report: Proof.context -> Position.T -> Markup.T -> unit
+  val reports_text: Proof.context -> Position.report_text list -> unit
   val reports: Proof.context -> Position.report list -> unit
 end;
 
@@ -53,6 +54,7 @@
 fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
 fun report ctxt pos markup = report_text ctxt pos markup "";
 
+fun reports_text ctxt reps = if is_visible ctxt then Position.reports_text reps else ();
 fun reports ctxt reps = if is_visible ctxt then Position.reports reps else ();
 
 end;