--- 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)