# HG changeset patch
# User wenzelm
# Date 1753726426 -7200
# Node ID f4bc5313c8216d2d3f37982686d0b04e946fd77b
# Parent  f4d263dc44421aa0730e12e7ba88e539a0b9d1d8
clarified modules;

diff -r f4d263dc4442 -r f4bc5313c821 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Jul 28 20:08:26 2025 +0200
+++ b/src/Pure/PIDE/editor.scala	Mon Jul 28 20:13:46 2025 +0200
@@ -93,6 +93,15 @@
 
   def output_state(): Boolean
 
+  def output_messages(results: Command.Results): List[XML.Elem] = {
+    val (states, other) =
+      results.iterator.map(_._2).filterNot(Protocol.is_result).toList
+        .partition(Protocol.is_state)
+    val (urgent, regular) = other.partition(Protocol.is_urgent)
+
+    urgent ::: (if (output_state()) states else Nil) ::: regular
+  }
+
 
   /* overlays */
 
diff -r f4d263dc4442 -r f4bc5313c821 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Jul 28 20:08:26 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Jul 28 20:13:46 2025 +0200
@@ -95,15 +95,6 @@
     legacy_pri -> Color.legacy_message,
     error_pri -> Color.error_message)
 
-  def output_messages(results: Command.Results, output_state: Boolean): List[XML.Elem] = {
-    val (states, other) =
-      results.iterator.map(_._2).filterNot(Protocol.is_result).toList
-        .partition(Protocol.is_state)
-    val (urgent, regular) = other.partition(Protocol.is_urgent)
-
-    urgent ::: (if (output_state) states else Nil) ::: regular
-  }
-
 
   /* text color */
 
diff -r f4d263dc4442 -r f4bc5313c821 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 28 20:08:26 2025 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 28 20:13:46 2025 +0200
@@ -29,9 +29,9 @@
             case None => Some(Nil)
             case Some(command) =>
               if (restriction.isEmpty || restriction.get.contains(command)) {
-                val output_state = server.editor.output_state()
-                Some(Rendering.output_messages(snapshot.command_results(command), output_state))
-              } else None
+                Some(server.editor.output_messages(snapshot.command_results(command)))
+              }
+              else None
           }
       }
       
diff -r f4d263dc4442 -r f4bc5313c821 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 28 20:08:26 2025 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 28 20:13:46 2025 +0200
@@ -44,7 +44,7 @@
         if restriction.isEmpty || restriction.get.contains(command)
       } {
         val results = snapshot.command_results(command)
-        val new_output = Rendering.output_messages(results, PIDE.editor.output_state())
+        val new_output = PIDE.editor.output_messages(results)
         if (current_output != new_output) {
           output.pretty_text_area.update(snapshot, results, new_output)
           current_output = new_output