src/Tools/jEdit/src/plugin.scala
changeset 56316 b1cf8ddc2e04
parent 56208 06cc31dff138
child 56387 d92eb5c3960d
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Mar 29 10:17:09 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Mar 29 10:49:32 2014 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4    @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty))
     1.5  
     1.6    def options_changed() { plugin.options_changed() }
     1.7 +  def deps_changed() { plugin.deps_changed() }
     1.8  
     1.9    def resources(): JEdit_Resources =
    1.10      session.resources.asInstanceOf[JEdit_Resources]
    1.11 @@ -168,13 +169,19 @@
    1.12  
    1.13  class Plugin extends EBPlugin
    1.14  {
    1.15 -  /* options */
    1.16 +  /* global changes */
    1.17  
    1.18 -  def options_changed() {
    1.19 +  def options_changed()
    1.20 +  {
    1.21      PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
    1.22      Swing_Thread.later { delay_load.invoke() }
    1.23    }
    1.24  
    1.25 +  def deps_changed()
    1.26 +  {
    1.27 +    Swing_Thread.later { delay_load.invoke() }
    1.28 +  }
    1.29 +
    1.30  
    1.31    /* theory files */
    1.32