--- 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 */
--- 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 */
--- 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
}
}
--- 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