changeset 65190 | 0dd2ad9dbfc2 |
parent 65145 | 576d52aa0a78 |
child 65213 | 51c0f094dc02 |
--- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 11 20:22:43 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 11 22:19:22 2017 +0100 @@ -436,14 +436,6 @@ }) } - 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 */