--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Nov 08 13:27:26 2024 +0100
@@ -46,9 +46,7 @@
}
private val sledgehammer =
- new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status,
- (snapshot, results, output) =>
- pretty_text_area.update(snapshot, results, Pretty.separate(output)))
+ new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status, pretty_text_area.update)
/* resize */