tuned;
authorwenzelm
Thu, 26 Nov 2020 17:01:19 +0100
changeset 72727 2da1993fe903
parent 72726 ec6a27bbdab8
child 72728 caa182bdab7a
tuned;
src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Thu Nov 26 16:51:40 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Thu Nov 26 17:01:19 2020 +0100
@@ -97,8 +97,8 @@
   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(_))
+      results.iterator.map(_._2).filterNot(Protocol.is_result).toList
+        .partition(Protocol.is_state)
     states ::: other
   }