# HG changeset patch
# User wenzelm
# Date 1489267162 -3600
# Node ID 0dd2ad9dbfc2ac32ffa1e093b6a5634371ebfeaf
# Parent  41d2452845fcba82293da2c8e228c8d4e42f6f89
tuned;

diff -r 41d2452845fc -r 0dd2ad9dbfc2 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sat Mar 11 20:22:43 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sat Mar 11 22:19:22 2017 +0100
@@ -78,7 +78,7 @@
   }
 
 
-  /* message priorities */
+  /* output messages */
 
   val state_pri = 1
   val writeln_pri = 2
@@ -120,6 +120,14 @@
     legacy_pri -> Color.legacy_message,
     error_pri -> Color.error_message)
 
+  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 */
 
diff -r 41d2452845fc -r 0dd2ad9dbfc2 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 */
 
diff -r 41d2452845fc -r 0dd2ad9dbfc2 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Mar 11 20:22:43 2017 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Mar 11 22:19:22 2017 +0100
@@ -65,10 +65,8 @@
       }
 
     val new_output =
-      if (!restriction.isDefined || restriction.get.contains(new_command)) {
-        val rendering = JEdit_Rendering(new_snapshot, PIDE.options.value)
-        rendering.output_messages(new_results)
-      }
+      if (!restriction.isDefined || restriction.get.contains(new_command))
+        Rendering.output_messages(new_results)
       else current_output
 
     if (new_output != current_output)