equal
deleted
inserted
replaced
81 option active_color : string = "DCDCDCFF" |
81 option active_color : string = "DCDCDCFF" |
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 |
87 |
87 option tfree_color : string = "A020F0FF" |
88 option tfree_color : string = "A020F0FF" |
88 option tvar_color : string = "A020F0FF" |
89 option tvar_color : string = "A020F0FF" |
89 option free_color : string = "0000FFFF" |
90 option free_color : string = "0000FFFF" |
90 option skolem_color : string = "D2691EFF" |
91 option skolem_color : string = "D2691EFF" |