src/Tools/jEdit/etc/options
changeset 55924 fd5e3f93bae4
parent 55919 2eb8c13339a5
child 56064 7658489047e3
equal deleted inserted replaced
55923:4bdae9403baf 55924:fd5e3f93bae4
    82 option active_hover_color : string = "9DC75DFF"
    82 option active_hover_color : string = "9DC75DFF"
    83 option active_result_color : string = "999966FF"
    83 option active_result_color : string = "999966FF"
    84 option keyword1_color : string = "006699FF"
    84 option keyword1_color : string = "006699FF"
    85 option keyword2_color : string = "009966FF"
    85 option keyword2_color : string = "009966FF"
    86 option keyword3_color : string = "0099FFFF"
    86 option keyword3_color : string = "0099FFFF"
    87 option quasi_keyword_color : string = "66CCFFFF"
    87 option quasi_keyword_color : string = "9966FFFF"
    88 option caret_invisible_color : string = "50000080"
    88 option caret_invisible_color : string = "50000080"
    89 option completion_color : string = "0000FFFF"
    89 option completion_color : string = "0000FFFF"
    90 
    90 
    91 option tfree_color : string = "A020F0FF"
    91 option tfree_color : string = "A020F0FF"
    92 option tvar_color : string = "A020F0FF"
    92 option tvar_color : string = "A020F0FF"