# HG changeset patch
# User wenzelm
# Date 1406379174 -7200
# Node ID 9616643a3032285035920d181189cd3b740e4349
# Parent  5b652fd305d44798682f52eb1a3298dfb557aaaf
output state first -- avoid fluctuation wrt. warnings, errors, etc.;

diff -r 5b652fd305d4 -r 9616643a3032 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Jul 25 21:44:03 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Jul 26 14:52:54 2014 +0200
@@ -610,7 +610,12 @@
   }
 
   def output_messages(results: Command.Results): List[XML.Tree] =
-    results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
+  {
+    val (states, other) =
+      results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
+        .partition(Protocol.is_state(_))
+    states ::: other
+  }
 
 
   /* text background */