clarified Editor.Output: more uniform handling in Isabelle/jEdit and Isabelle/VSCode;

--- a/src/Pure/PIDE/editor.scala	Mon Jul 28 20:15:13 2025 +0200
+++ b/src/Pure/PIDE/editor.scala	Mon Jul 28 21:13:09 2025 +0200
@@ -7,6 +7,21 @@
 package isabelle
 
 
+object Editor {
+  /* output messages */
+
+  object Output {
+    val none: Output = Output(defined = false)
+    val init: Output = Output()
+  }
+
+  sealed case class Output(
+    results: Command.Results = Command.Results.empty,
+    messages: List[XML.Elem] = Nil,
+    defined: Boolean = true
+  )
+}
+
 abstract class Editor[Context] {
   /* PIDE session and document model */
 
@@ -93,13 +108,30 @@
 
   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)
+  def output(
+    snapshot: Document.Snapshot,
+    offset: Text.Offset,
+    restriction: Option[Set[Command]] = None
+  ): Editor.Output = {
+    if (snapshot.is_outdated) Editor.Output.none
+    else {
+      snapshot.current_command(snapshot.node_name, offset) match {
+        case None => Editor.Output.init
+        case Some(command) =>
+          if (restriction.isEmpty || restriction.get.contains(command)) {
+            val results = snapshot.command_results(command)
 
-    urgent ::: (if (output_state()) states else Nil) ::: regular
+            val (states, other) =
+              results.iterator.map(_._2).filterNot(Protocol.is_result).toList
+                .partition(Protocol.is_state)
+            val (urgent, regular) = other.partition(Protocol.is_urgent)
+            val messages = urgent ::: (if (output_state()) states else Nil) ::: regular
+
+            Editor.Output(results = results, messages = messages)
+          }
+          else Editor.Output.none
+      }
+    }
   }
 
 

--- a/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 28 20:15:13 2025 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 28 21:13:09 2025 +0200
@@ -20,22 +20,14 @@
     pretty_panel_.value.getOrElse(error("No Pretty Panel for Dynamic Output"))
 
   private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = {
-    val maybe_output =
+    val output =
       server.resources.get_caret() match {
-        case None => Some(Nil)
+        case None => Editor.Output.init
         case Some(caret) =>
           val snapshot = server.resources.snapshot(caret.model)
-          snapshot.current_command(caret.node_name, caret.offset) match {
-            case None => Some(Nil)
-            case Some(command) =>
-              if (restriction.isEmpty || restriction.get.contains(command)) {
-                Some(server.editor.output_messages(snapshot.command_results(command)))
-              }
-              else None
-          }
+          server.editor.output(snapshot, caret.offset)
       }
-      
-    maybe_output.foreach(pretty_panel.refresh)
+    if (output.defined) pretty_panel.refresh(output.messages)
   }
 
 

--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 28 20:15:13 2025 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 28 21:13:09 2025 +0200
@@ -37,17 +37,12 @@
 
   private def handle_update(restriction: Option[Set[Command]] = None): Unit =
     GUI_Thread.require {
-      for {
-        snapshot <- PIDE.editor.current_node_snapshot(view)
-        if !snapshot.is_outdated
-        command <- PIDE.editor.current_command(view, snapshot)
-        if restriction.isEmpty || restriction.get.contains(command)
-      } {
-        val results = snapshot.command_results(command)
-        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
+      val offset = view.getTextArea.getCaretPosition
+      for (snapshot <- PIDE.editor.current_node_snapshot(view)) {
+        val output = PIDE.editor.output(snapshot, offset, restriction = restriction)
+        if (output.defined && current_output != output.messages) {
+          dockable.output.pretty_text_area.update(snapshot, output.results, output.messages)
+          current_output = output.messages
         }
       }
     }