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,