diff -r ddbb89e7621d -r 7283f41d05ab src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Jan 06 11:58:29 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Jan 06 13:27:18 2017 +0100
@@ -73,10 +73,10 @@
     GUI_Thread.require { jEdit.getActiveView() }
 
   override def current_node(view: View): Option[Document.Node.Name] =
-    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
+    GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) }
 
   override def current_node_snapshot(view: View): Option[Document.Snapshot] =
-    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
+    GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) }
 
   override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
   {
@@ -84,7 +84,7 @@
 
     JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>
-        PIDE.document_model(buffer) match {
+        Document_Model.get(buffer) match {
           case Some(model) => model.snapshot
           case None => session.snapshot(name)
         }
@@ -113,7 +113,7 @@
         }
         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
       case _ =>
-        PIDE.document_model(buffer) match {
+        Document_Model.get(buffer) match {
           case Some(model) if !model.is_theory =>
             snapshot.version.nodes.commands_loading(model.node_name) match {
               case cmd :: _ => Some(cmd)