allow embedded reports in regular prover messages, to avoid side-effects for errors for example;

--- a/src/Pure/Isar/proof_context.ML	Fri Sep 17 17:09:31 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Sep 17 17:10:44 2010 +0200
@@ -734,8 +734,8 @@
 local
 
 fun parse_failed ctxt pos msg kind =
- (Context_Position.report ctxt Markup.bad pos;
-  cat_error msg ("Failed to parse " ^ kind));
+  cat_error msg ("Failed to parse " ^ kind ^
+    Markup.markup Markup.report (Context_Position.reported_text ctxt Markup.bad pos ""));
 
 fun parse_sort ctxt text =
   let

--- a/src/Pure/PIDE/command.scala	Fri Sep 17 17:09:31 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Sep 17 17:10:44 2010 +0200
@@ -60,8 +60,10 @@
           atts match {
             case Markup.Serial(i) =>
               val result = XML.Elem(Markup(name, Position.purge(atts)), body)
-              (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
-                (st, range) => st.add_markup(Text.Info(range, result)))
+              val st1 =
+                (add_result(i, result) /: Isar_Document.message_positions(command, message))(
+                  (st, range) => st.add_markup(Text.Info(range, result)))
+              (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
             case _ => System.err.println("Ignored message without serial number: " + message); this
           }
       }

--- a/src/Pure/PIDE/isar_document.scala	Fri Sep 17 17:09:31 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 17 17:10:44 2010 +0200
@@ -56,35 +56,42 @@
   }
 
 
-  /* messages */
+  /* result messages */
 
   def clean_message(body: XML.Body): XML.Body =
     body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
       { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
 
+  def message_reports(msg: XML.Tree): List[XML.Elem] =
+    msg match {
+      case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
+      case XML.Elem(_, body) => body.flatMap(message_reports)
+      case XML.Text(_) => Nil
+    }
+
 
   /* reported positions */
 
-  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
-
-  private def is_state(msg: XML.Tree): Boolean =
+  def is_state(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
       case _ => false
     }
 
-  def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
+  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+
+  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   {
-    def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
+    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
       tree match {
         case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
         if include_pos(name) && id == command.id =>
           val range = command.decode(raw_range).restrict(command.range)
-          body.foldLeft(if (range.is_singularity) set else set + range)(reported)
-        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(reported)
+          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
+        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
         case _ => set
       }
-    val set = reported(Set.empty, message)
+    val set = positions(Set.empty, message)
     if (set.isEmpty && !is_state(message))
       set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
     else set

--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 17:09:31 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 17:10:44 2010 +0200
@@ -8,6 +8,8 @@
 .error { background-color: #FFC1C1; }
 .debug { background-color: #FFE4E1; }
 
+.report { display: none; }
+
 .hilite { background-color: #FFFACD; }
 
 .keyword { font-weight: bold; color: #009966; }