src/Tools/jEdit/src/output_dockable.scala

--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Jun 13 20:16:39 2017 +0200
@@ -47,11 +47,11 @@
     GUI_Thread.require {}
 
     for {
-      snapshot <- JEdit_Editor.current_node_snapshot(view)
+      snapshot <- PIDE.editor.current_node_snapshot(view)
       if follow && !snapshot.is_outdated
     } {
       val (command, results) =
-        JEdit_Editor.current_command(view, snapshot) match {
+        PIDE.editor.current_command(view, snapshot) match {
           case Some(command) => (command, snapshot.command_results(command))
           case None => (Command.empty, Command.Results.empty)
         }
@@ -77,8 +77,8 @@
     if (output_state != b) {
       PIDE.options.bool("editor_output_state") = b
       PIDE.session.update_options(PIDE.options.value)
-      JEdit_Editor.flush(hidden = true)
-      JEdit_Editor.flush()
+      PIDE.editor.flush(hidden = true)
+      PIDE.editor.flush()
     }
   }