src/Tools/jEdit/src/query_dockable.scala
changeset 65246 848965b5befc
parent 63805 c272680df665
child 66082 2d12a730a380
--- a/src/Tools/jEdit/src/query_dockable.scala	Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Tue Mar 14 21:43:54 2017 +0100
@@ -77,7 +77,7 @@
     private val process_indicator = new Process_Indicator
 
     val query_operation =
-      new Query_Operation(PIDE.editor, view, "find_theorems",
+      new Query_Operation(JEdit_Editor, view, "find_theorems",
         consume_status(process_indicator, _),
         (snapshot, results, body) =>
           pretty_text_area.update(snapshot, results, Pretty.separate(body)))
@@ -143,7 +143,7 @@
     private val process_indicator = new Process_Indicator
 
     val query_operation =
-      new Query_Operation(PIDE.editor, view, "find_consts",
+      new Query_Operation(JEdit_Editor, view, "find_consts",
         consume_status(process_indicator, _),
         (snapshot, results, body) =>
           pretty_text_area.update(snapshot, results, Pretty.separate(body)))
@@ -226,7 +226,7 @@
     private val process_indicator = new Process_Indicator
 
     val query_operation =
-      new Query_Operation(PIDE.editor, view, "print_operation",
+      new Query_Operation(JEdit_Editor, view, "print_operation",
         consume_status(process_indicator, _),
         (snapshot, results, body) =>
           pretty_text_area.update(snapshot, results, Pretty.separate(body)))