# HG changeset patch
# User wenzelm
# Date 1489523185 -3600
# Node ID ba5ce07e06a7c15fb86d79d64b106c90b6b22d4d
# Parent  63a64779d586b7675f006c8943e41dfb10fa4638
proper plugin access;

diff -r 63a64779d586 -r ba5ce07e06a7 src/Tools/jEdit/src/document_model.scala
--- 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()
     }
   }
diff -r 63a64779d586 -r ba5ce07e06a7 src/Tools/jEdit/src/jedit_resources.scala
--- 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()
   }
 }
diff -r 63a64779d586 -r ba5ce07e06a7 src/Tools/jEdit/src/plugin.scala
--- 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]