Rudimentary preferences for editor colours. No property change listeners
yet, so the editor(s) must be restarted for colour changes to take
effect.