src/Tools/jEdit/src/sledgehammer_dockable.scala
changeset 83419 0ac8a8a3793b
parent 83022 5fe1d566794e
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Mon Oct 27 15:24:25 2025 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Mon Oct 27 15:36:47 2025 +0100
@@ -51,7 +51,7 @@
 
   private val sledgehammer =
     new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status,
-      output.pretty_text_area.update)
+      output.pretty_text_area.update_output)
 
 
   /* controls */