org.gjt.sp.jedit.EditPane.propertiesChanged()
org.gjt.sp.jedit.options.ViewOptionPane._init()
org.gjt.sp.jedit.options.ViewOptionPane._save()