# HG changeset patch
# User wenzelm
# Date 1348067245 -7200
# Node ID 638cefe3ee99d4517480eae03d459bd1973c8488
# Parent  fad4724230ce141ad8c5eb9da7d4360cc24dc23d
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);

diff -r fad4724230ce -r 638cefe3ee99 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Sep 19 14:47:15 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Sep 19 17:07:25 2012 +0200
@@ -70,8 +70,8 @@
                 else
                   (st0 /: Protocol.message_positions(command, message))(
                     (st, range) => st.add_markup(Text.Info(range, result)))
-              val st2 = (st1 /: Protocol.message_reports(message))(_ + _)
-              st2
+
+              st1
             case _ => System.err.println("Ignored message without serial number: " + message); this
           }
       }
diff -r fad4724230ce -r 638cefe3ee99 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Sep 19 14:47:15 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Sep 19 17:07:25 2012 +0200
@@ -119,13 +119,17 @@
   /* result messages */
 
   def clean_message(body: XML.Body): XML.Body =
-    body filter { case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false case _ => true } map
-      { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
+    body filter {
+      case XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => false
+      case XML.Elem(Markup(Isabelle_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(Isabelle_Markup.REPORT, _), _) => List(elem)
-      case XML.Elem(_, body) => body.flatMap(message_reports)
+  def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
+    body flatMap {
+      case XML.Elem(Markup(Isabelle_Markup.REPORT, ps), ts) =>
+        List(XML.Elem(Markup(Isabelle_Markup.REPORT, props ::: ps), ts))
+      case XML.Elem(_, ts) => message_reports(props, ts)
       case XML.Text(_) => Nil
     }
 
diff -r fad4724230ce -r 638cefe3ee99 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Wed Sep 19 14:47:15 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala	Wed Sep 19 17:07:25 2012 +0200
@@ -109,8 +109,10 @@
     if (kind == Isabelle_Markup.PROTOCOL)
       receiver(new Output(XML.Elem(Markup(kind, props), body)))
     else {
-      val msg = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
-      receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
+      val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
+      val reports = Protocol.message_reports(props, body)
+      for (msg <- main :: reports)
+        receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
     }
   }
 
diff -r fad4724230ce -r 638cefe3ee99 src/Tools/jEdit/etc/isabelle-jedit.css
--- a/src/Tools/jEdit/etc/isabelle-jedit.css	Wed Sep 19 14:47:15 2012 +0200
+++ b/src/Tools/jEdit/etc/isabelle-jedit.css	Wed Sep 19 17:07:25 2012 +0200
@@ -7,8 +7,6 @@
 .warning_message { background-color: #EEE8AA; }
 .error_message { background-color: #FFC1C1; }
 
-.report { display: none; }
-
 .intensify { background-color: #FFCC66; }
 
 .keyword { font-weight: bold; color: #009966; }