1.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Jul 25 21:44:03 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Jul 26 14:52:54 2014 +0200
     1.3 @@ -610,7 +610,12 @@
     1.4    }
     1.5  
     1.6    def output_messages(results: Command.Results): List[XML.Tree] =
     1.7 -    results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
     1.8 +  {
     1.9 +    val (states, other) =
    1.10 +      results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
    1.11 +        .partition(Protocol.is_state(_))
    1.12 +    states ::: other
    1.13 +  }
    1.14  
    1.15  
    1.16    /* text background */