# HG changeset patch
# User wenzelm
# Date 1753726106 -7200
# Node ID f4d263dc44421aa0730e12e7ba88e539a0b9d1d8
# Parent  710235d4db8a4bd39c3fb7c3f142a19365c890d0
clarified signature: more explicit operations;

diff -r 710235d4db8a -r f4d263dc4442 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Jul 28 19:50:44 2025 +0200
+++ b/src/Pure/PIDE/editor.scala	Mon Jul 28 20:08:26 2025 +0200
@@ -89,6 +89,11 @@
   def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
 
 
+  /* output messages */
+
+  def output_state(): Boolean
+
+
   /* overlays */
 
   def node_overlays(name: Document.Node.Name): Document.Node.Overlays
diff -r 710235d4db8a -r f4d263dc4442 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 28 19:50:44 2025 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 28 20:08:26 2025 +0200
@@ -29,7 +29,7 @@
             case None => Some(Nil)
             case Some(command) =>
               if (restriction.isEmpty || restriction.get.contains(command)) {
-                val output_state = server.resources.options.bool("editor_output_state")
+                val output_state = server.editor.output_state()
                 Some(Rendering.output_messages(snapshot.command_results(command), output_state))
               } else None
           }
diff -r 710235d4db8a -r f4d263dc4442 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Mon Jul 28 19:50:44 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Jul 28 20:08:26 2025 +0200
@@ -587,6 +587,11 @@
       current_command(snapshot)
 
 
+    /* output messages */
+
+    override def output_state(): Boolean = resources.options.bool("editor_output_state")
+
+
     /* overlays */
 
     override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
diff -r 710235d4db8a -r f4d263dc4442 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Jul 28 19:50:44 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Jul 28 20:08:26 2025 +0200
@@ -89,6 +89,11 @@
     }
 
 
+  /* output messages */
+
+  override def output_state(): Boolean = JEdit_Options.output_state()
+
+
   /* overlays */
 
   override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
diff -r 710235d4db8a -r f4d263dc4442 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 28 19:50:44 2025 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 28 20:08:26 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, JEdit_Options.output_state())
+        val new_output = Rendering.output_messages(results, PIDE.editor.output_state())
         if (current_output != new_output) {
           output.pretty_text_area.update(snapshot, results, new_output)
           current_output = new_output