# HG changeset patch
# User wenzelm
# Date 1761574592 -3600
# Node ID b51e4a52689770d8b9d24b51fefc83b671b49653
# Parent  c7849fa2ece0a653cfa9bf991900817c8fe48180
clarified signature;

diff -r c7849fa2ece0 -r b51e4a526897 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Oct 27 12:37:31 2025 +0100
+++ b/src/Pure/PIDE/editor.scala	Mon Oct 27 15:16:32 2025 +0100
@@ -16,6 +16,7 @@
   }
 
   sealed case class Output(
+    snapshot: Document.Snapshot = Document.Snapshot.init,
     results: Command.Results = Command.Results.empty,
     messages: List[XML.Elem] = Nil,
     defined: Boolean = true
@@ -138,7 +139,7 @@
               val (urgent, regular) = other.partition(Protocol.is_urgent)
               urgent ::: (if (output_state()) states else Nil) ::: regular
             }
-            Editor.Output(results = results, messages = messages)
+            Editor.Output(snapshot = snapshot, results = results, messages = messages)
           }
           else Editor.Output.none
       }
diff -r c7849fa2ece0 -r b51e4a526897 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Oct 27 12:37:31 2025 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Oct 27 15:16:32 2025 +0100
@@ -41,7 +41,7 @@
       for (snapshot <- PIDE.editor.current_node_snapshot(view)) {
         val output = PIDE.editor.output(snapshot, caret_offset, restriction = restriction)
         if (output.defined && current_output != output.messages) {
-          dockable.output.pretty_text_area.update(snapshot, output.results, output.messages)
+          dockable.output.pretty_text_area.update_output(output)
           current_output = output.messages
         }
       }
diff -r c7849fa2ece0 -r b51e4a526897 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Oct 27 12:37:31 2025 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Oct 27 15:16:32 2025 +0100
@@ -241,6 +241,9 @@
     refresh()
   }
 
+  def update_output(output: Editor.Output): Unit =
+    if (output.defined) update(output.snapshot, output.results, output.messages)
+
   def update(
     base_snapshot: Document.Snapshot,
     base_results: Command.Results,