--- a/src/Pure/PIDE/rendering.scala Sat Mar 11 20:22:43 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala Sat Mar 11 22:19:22 2017 +0100
@@ -78,7 +78,7 @@
}
- /* message priorities */
+ /* output messages */
val state_pri = 1
val writeln_pri = 2
@@ -120,6 +120,14 @@
legacy_pri -> Color.legacy_message,
error_pri -> Color.error_message)
+ def output_messages(results: Command.Results): List[XML.Tree] =
+ {
+ val (states, other) =
+ results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
+ .partition(Protocol.is_state(_))
+ states ::: other
+ }
+
/* text color */