src/Tools/jEdit/src/jedit_rendering.scala

--- 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 */