changeset 66082 | 2d12a730a380 |
parent 65246 | 848965b5befc |
child 66205 | e9fa94f43a15 |
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Jun 13 15:11:01 2017 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Jun 13 20:16:39 2017 +0200 @@ -49,7 +49,7 @@ } private val sledgehammer = - new Query_Operation(JEdit_Editor, view, "sledgehammer", consume_status _, + new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _, (snapshot, results, body) => pretty_text_area.update(snapshot, results, Pretty.separate(body)))