equal
deleted
inserted
replaced
70 option inner_numeral_color : string = "FF0000FF" |
70 option inner_numeral_color : string = "FF0000FF" |
71 option inner_quoted_color : string = "D2691EFF" |
71 option inner_quoted_color : string = "D2691EFF" |
72 option inner_comment_color : string = "8B0000FF" |
72 option inner_comment_color : string = "8B0000FF" |
73 option dynamic_color : string = "7BA428FF" |
73 option dynamic_color : string = "7BA428FF" |
74 |
74 |
|
75 |
|
76 section "Icons" |
|
77 |
|
78 (* jEdit/Tango *) |
|
79 (* |
|
80 option tooltip_close_icon : string = "16x16/actions/document-close.png" |
|
81 option tooltip_detach_icon : string = "16x16/actions/window-new.png" |
|
82 option gutter_warning_icon : string = "16x16/status/dialog-information.png" |
|
83 option gutter_legacy_icon : string = "16x16/status/dialog-warning.png" |
|
84 option gutter_error_icon : string = "16x16/status/dialog-error.png" |
|
85 *) |
|
86 |
|
87 (* IntelliJ IDEA *) |
|
88 option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png" |
|
89 option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png" |
|
90 option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png" |
|
91 option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png" |
|
92 option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png" |
|
93 |