--- 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"