proper plugin access;
authorwenzelm
Tue Mar 14 21:26:25 2017 +0100 (2017-03-14 ago)
changeset 65243ba5ce07e06a7
parent 65242 63a64779d586
child 65244 1f53b9470116
proper plugin access;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Mar 14 21:24:33 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 14 21:26:25 2017 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4              }
     1.5          })
     1.6      if (changed) {
     1.7 -      PIDE.options_changed()
     1.8 +      PIDE.plugin.options_changed()
     1.9        PIDE.editor.flush()
    1.10      }
    1.11    }
     2.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Mar 14 21:24:33 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Mar 14 21:26:25 2017 +0100
     2.3 @@ -145,6 +145,6 @@
     2.4        GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) }
     2.5      if (change.deps_changed ||
     2.6          PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version.nodes).nonEmpty)
     2.7 -      PIDE.deps_changed()
     2.8 +      PIDE.plugin.deps_changed()
     2.9    }
    2.10  }
     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 21:24:33 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 21:26:25 2017 +0100
     3.3 @@ -38,9 +38,6 @@
     3.4  
     3.5    @volatile var session: Session = new Session(JEdit_Resources.empty)
     3.6  
     3.7 -  def options_changed() { if (plugin != null) plugin.options_changed() }
     3.8 -  def deps_changed() { if (plugin != null) plugin.deps_changed() }
     3.9 -
    3.10    def resources(): JEdit_Resources =
    3.11      session.resources.asInstanceOf[JEdit_Resources]
    3.12