# HG changeset patch
# User wenzelm
# Date 1660393799 -7200
# Node ID f8c412a45af8705950258dccaeec9e3fc0453f44
# Parent  29441f2bfe810f455e329506ac9187ee506c2d9b
more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;

diff -r 29441f2bfe81 -r f8c412a45af8 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sat Aug 13 12:32:38 2022 +0200
+++ b/src/Pure/PIDE/rendering.scala	Sat Aug 13 14:29:59 2022 +0200
@@ -95,11 +95,11 @@
     legacy_pri -> Color.legacy_message,
     error_pri -> Color.error_message)
 
-  def output_messages(results: Command.Results): List[XML.Elem] = {
+  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)
-    states ::: other
+    (if (output_state) states else Nil) ::: other
   }
 
 
diff -r 29441f2bfe81 -r f8c412a45af8 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Sat Aug 13 12:32:38 2022 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Sat Aug 13 14:29:59 2022 +0200
@@ -27,9 +27,10 @@
                 case None => copy(output = Nil)
                 case Some(command) =>
                   copy(output =
-                    if (restriction.isEmpty || restriction.get.contains(command))
-                      Rendering.output_messages(snapshot.command_results(command))
-                    else output)
+                    if (restriction.isEmpty || restriction.get.contains(command)) {
+                      val output_state = resources.options.bool("editor_output_state")
+                      Rendering.output_messages(snapshot.command_results(command), output_state)
+                    } else output)
               }
             }
             else this
diff -r 29441f2bfe81 -r f8c412a45af8 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 13 12:32:38 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 13 14:29:59 2022 +0200
@@ -51,7 +51,7 @@
 
       val new_output =
         if (restriction.isEmpty || restriction.get.contains(command))
-          Rendering.output_messages(results)
+          Rendering.output_messages(results, output_state)
         else current_output
 
       if (current_output != new_output) {