src/Tools/jEdit/src/state_dockable.scala

   set_content(pretty_text_area)
 
   override def detach_operation = pretty_text_area.detach_operation
 
   private val print_state =
-    new Query_Operation(JEdit_Editor, view, "print_state", _ => (),
+    new Query_Operation(PIDE.editor, view, "print_state", _ => (),
       (snapshot, results, body) =>
         pretty_text_area.update(snapshot, results, Pretty.separate(body)))
 
 
   /* resize */

   {
     GUI_Thread.require {}
 
     Document_Model.get(view.getBuffer).map(_.snapshot()) match {
       case Some(snapshot) =>
-        (JEdit_Editor.current_command(view, snapshot), print_state.get_location) match {
+        (PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
           case (Some(command1), Some(command2)) if command1.id == command2.id =>
           case _ => update_request()
         }
       case None =>
     }