# HG changeset patch
# User wenzelm
# Date 1447073369 -3600
# Node ID 2abbe7d700e96b435ee5ec0cc1b0bfe7460c59cb
# Parent  a2f0f659a3c2c7076b59e5a72b215821d3d7e2f4
suppress already persistent state output as well;

diff -r a2f0f659a3c2 -r 2abbe7d700e9 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sun Nov 08 14:41:07 2015 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Nov 09 13:49:29 2015 +0100
@@ -678,7 +678,7 @@
     val (states, other) =
       results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
         .partition(Protocol.is_state(_))
-    states ::: other
+    if (options.bool("editor_output_state")) states ::: other else other
   }