# HG changeset patch
# User wenzelm
# Date 1606406479 -3600
# Node ID 2da1993fe903b695f3e4bc7337d1997349ddc91c
# Parent  ec6a27bbdab86d158dffceebd51a1113597c312c
tuned;

diff -r ec6a27bbdab8 -r 2da1993fe903 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
   }