src/Tools/jEdit/src/jedit_resources.scala
changeset 56316 b1cf8ddc2e04
parent 56208 06cc31dff138
child 56457 eea4bbe15745
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sat Mar 29 10:17:09 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sat Mar 29 10:49:32 2014 +0100
     1.3 @@ -117,7 +117,10 @@
     1.4  
     1.5    /* theory text edits */
     1.6  
     1.7 -  override def syntax_changed(): Unit =
     1.8 -    Swing_Thread.later { jEdit.propertiesChanged() }
     1.9 +  override def commit(change: Session.Change)
    1.10 +  {
    1.11 +    if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
    1.12 +    if (change.deps_changed) PIDE.deps_changed()
    1.13 +  }
    1.14  }
    1.15