--- a/src/Tools/jEdit/src/document_model.scala Tue Mar 14 21:24:33 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Mar 14 21:26:25 2017 +0100
@@ -182,7 +182,7 @@
}
})
if (changed) {
- PIDE.options_changed()
+ PIDE.plugin.options_changed()
PIDE.editor.flush()
}
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Tue Mar 14 21:24:33 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Mar 14 21:26:25 2017 +0100
@@ -145,6 +145,6 @@
GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) }
if (change.deps_changed ||
PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version.nodes).nonEmpty)
- PIDE.deps_changed()
+ PIDE.plugin.deps_changed()
}
}
--- a/src/Tools/jEdit/src/plugin.scala Tue Mar 14 21:24:33 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Mar 14 21:26:25 2017 +0100
@@ -38,9 +38,6 @@
@volatile var session: Session = new Session(JEdit_Resources.empty)
- def options_changed() { if (plugin != null) plugin.options_changed() }
- def deps_changed() { if (plugin != null) plugin.deps_changed() }
-
def resources(): JEdit_Resources =
session.resources.asInstanceOf[JEdit_Resources]