Skip to content
Success

Changes

Summary

  1. tuned signature -- avoid warning during jEdit startup;
  2. more thorough change of syntax style extender: jEdit.propertiesChanged invalidates buffer chunk cache;
Changeset 66603:f6a1274be674 by wenzelm:
tuned signature -- avoid warning during jEdit startup;
The file was modified src/Tools/jEdit/src-base/plugin.scala (diff)
Changeset 66602:180b2e72601f by wenzelm:
more thorough change of syntax style extender: jEdit.propertiesChanged invalidates buffer chunk cache;
The file was modified src/Tools/jEdit/src-base/plugin.scala (diff)
The file was modified src/Tools/jEdit/src-base/syntax_style.scala (diff)
The file was modified src/Tools/jEdit/src/plugin.scala (diff)