src/Tools/jEdit/etc/options
changeset 62988 224e8d8a4fb8
parent 62986 9d2fae6b31cc
child 62991 35f1475e9ced
equal deleted inserted replaced
62987:dc8a8a7559e7 62988:224e8d8a4fb8
    97 option legacy_message_color : string = "EEE8AAFF"
    97 option legacy_message_color : string = "EEE8AAFF"
    98 option error_message_color : string = "FFC1C1FF"
    98 option error_message_color : string = "FFC1C1FF"
    99 option spell_checker_color : string = "0000FFFF"
    99 option spell_checker_color : string = "0000FFFF"
   100 option bad_color : string = "FF6A6A64"
   100 option bad_color : string = "FF6A6A64"
   101 option intensify_color : string = "FFCC6664"
   101 option intensify_color : string = "FFCC6664"
   102 option entity_def_color : string = "CCD9FFA0"
   102 option entity_color : string = "CCD9FF80"
   103 option entity_ref_color : string = "E6FFCCA0"
   103 option entity_def_color : string = "800080FF"
   104 option breakpoint_disabled_color : string = "CCCC0080"
   104 option breakpoint_disabled_color : string = "CCCC0080"
   105 option breakpoint_enabled_color : string = "FF9966FF"
   105 option breakpoint_enabled_color : string = "FF9966FF"
   106 option quoted_color : string = "8B8B8B19"
   106 option quoted_color : string = "8B8B8B19"
   107 option antiquoted_color : string = "FFC83219"
   107 option antiquoted_color : string = "FFC83219"
   108 option antiquote_color : string = "6600CCFF"
   108 option antiquote_color : string = "6600CCFF"