diff -r 4be23c432491 -r 9d2fae6b31cc src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Thu Apr 14 20:47:44 2016 +0200 +++ b/src/Tools/jEdit/etc/options Thu Apr 14 22:55:53 2016 +0200 @@ -99,6 +99,8 @@ option spell_checker_color : string = "0000FFFF" option bad_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" +option entity_def_color : string = "CCD9FFA0" +option entity_ref_color : string = "E6FFCCA0" option breakpoint_disabled_color : string = "CCCC0080" option breakpoint_enabled_color : string = "FF9966FF" option quoted_color : string = "8B8B8B19"