org.gjt.sp.jedit.View.propertiesChanged()
org.gjt.sp.jedit.options.StatusBarOptionPane._init()
org.gjt.sp.jedit.options.StatusBarOptionPane._save()