--- 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
}
}
--- 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
}
--- 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]))
}
}
--- 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; }