changeset 72727 | 2da1993fe903 |
parent 72692 | 22aeec526ffd |
child 72729 | 83411077c37b |
--- 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 }