| 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 */