diff -r 606ac3fae270 -r 3e235fab64db src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Sat Mar 11 12:48:37 2023 +0100 +++ b/src/Tools/jEdit/etc/options Sat Mar 11 13:31:16 2023 +0100 @@ -87,74 +87,74 @@ section "Rendering of Document Content" -option outdated_color : string = "EEE3E3FF" -option unprocessed_color : string = "FFA0A0FF" -option unprocessed1_color : string = "FFA0A032" -option running_color : string = "610061FF" -option running1_color : string = "61006164" -option bullet_color : string = "000000FF" -option tooltip_color : string = "FFFFE9FF" -option writeln_color : string = "C0C0C0FF" -option information_color : string = "C1DFEEFF" -option warning_color : string = "FF8C00FF" -option legacy_color : string = "FF8C00FF" -option error_color : string = "B22222FF" -option ok_color : string = "000000FF" -option failed_color : string = "B22222FF" -option writeln_message_color : string = "F0F0F0FF" -option information_message_color : string = "DCEAF3FF" -option tracing_message_color : string = "F0F8FFFF" -option warning_message_color : string = "EEE8AAFF" -option legacy_message_color : string = "EEE8AAFF" -option error_message_color : string = "FFC1C1FF" -option spell_checker_color : string = "0000FFFF" -option bad_color : string = "FF6A6A64" -option canceled_color : string = "FF6A6A64" -option intensify_color : string = "FFCC6664" -option entity_color : string = "CCD9FF80" -option entity_ref_color : string = "800080FF" -option breakpoint_disabled_color : string = "CCCC0080" -option breakpoint_enabled_color : string = "FF9966FF" -option quoted_color : string = "8B8B8B19" -option antiquoted_color : string = "FFC83219" -option antiquote_color : string = "6600CCFF" -option raw_text_color : string = "6600CCFF" -option plain_text_color : string = "CC6600FF" -option highlight_color : string = "50505032" -option hyperlink_color : string = "000000FF" -option active_color : string = "DCDCDCFF" -option active_hover_color : string = "9DC75DFF" -option active_result_color : string = "999966FF" -option keyword1_color : string = "006699FF" -option keyword2_color : string = "009966FF" -option keyword3_color : string = "0099FFFF" -option quasi_keyword_color : string = "9966FFFF" -option improper_color : string = "FF5050FF" -option operator_color : string = "323232FF" -option comment1_color : string = "CC0000FF" -option comment2_color : string = "FF8400FF" -option comment3_color : string = "6600CCFF" -option caret_debugger_color : string = "FF9966FF" -option caret_invisible_color : string = "50000080" -option completion_color : string = "0000FFFF" -option search_color : string = "66FFFF64" +option outdated_color : string = "EEE3E3FF" for color_dialog +option unprocessed_color : string = "FFA0A0FF" for color_dialog +option unprocessed1_color : string = "FFA0A032" for color_dialog +option running_color : string = "610061FF" for color_dialog +option running1_color : string = "61006164" for color_dialog +option bullet_color : string = "000000FF" for color_dialog +option tooltip_color : string = "FFFFE9FF" for color_dialog +option writeln_color : string = "C0C0C0FF" for color_dialog +option information_color : string = "C1DFEEFF" for color_dialog +option warning_color : string = "FF8C00FF" for color_dialog +option legacy_color : string = "FF8C00FF" for color_dialog +option error_color : string = "B22222FF" for color_dialog +option ok_color : string = "000000FF" for color_dialog +option failed_color : string = "B22222FF" for color_dialog +option writeln_message_color : string = "F0F0F0FF" for color_dialog +option information_message_color : string = "DCEAF3FF" for color_dialog +option tracing_message_color : string = "F0F8FFFF" for color_dialog +option warning_message_color : string = "EEE8AAFF" for color_dialog +option legacy_message_color : string = "EEE8AAFF" for color_dialog +option error_message_color : string = "FFC1C1FF" for color_dialog +option spell_checker_color : string = "0000FFFF" for color_dialog +option bad_color : string = "FF6A6A64" for color_dialog +option canceled_color : string = "FF6A6A64" for color_dialog +option intensify_color : string = "FFCC6664" for color_dialog +option entity_color : string = "CCD9FF80" for color_dialog +option entity_ref_color : string = "800080FF" for color_dialog +option breakpoint_disabled_color : string = "CCCC0080" for color_dialog +option breakpoint_enabled_color : string = "FF9966FF" for color_dialog +option quoted_color : string = "8B8B8B19" for color_dialog +option antiquoted_color : string = "FFC83219" for color_dialog +option antiquote_color : string = "6600CCFF" for color_dialog +option raw_text_color : string = "6600CCFF" for color_dialog +option plain_text_color : string = "CC6600FF" for color_dialog +option highlight_color : string = "50505032" for color_dialog +option hyperlink_color : string = "000000FF" for color_dialog +option active_color : string = "DCDCDCFF" for color_dialog +option active_hover_color : string = "9DC75DFF" for color_dialog +option active_result_color : string = "999966FF" for color_dialog +option keyword1_color : string = "006699FF" for color_dialog +option keyword2_color : string = "009966FF" for color_dialog +option keyword3_color : string = "0099FFFF" for color_dialog +option quasi_keyword_color : string = "9966FFFF" for color_dialog +option improper_color : string = "FF5050FF" for color_dialog +option operator_color : string = "323232FF" for color_dialog +option comment1_color : string = "CC0000FF" for color_dialog +option comment2_color : string = "FF8400FF" for color_dialog +option comment3_color : string = "6600CCFF" for color_dialog +option caret_debugger_color : string = "FF9966FF" for color_dialog +option caret_invisible_color : string = "50000080" for color_dialog +option completion_color : string = "0000FFFF" for color_dialog +option search_color : string = "66FFFF64" for color_dialog -option tfree_color : string = "A020F0FF" -option tvar_color : string = "A020F0FF" -option free_color : string = "0000FFFF" -option skolem_color : string = "D2691EFF" -option bound_color : string = "008000FF" -option var_color : string = "00009BFF" -option inner_numeral_color : string = "FF0000FF" -option inner_quoted_color : string = "FF00CCFF" -option inner_cartouche_color : string = "CC6600FF" -option dynamic_color : string = "7BA428FF" -option class_parameter_color : string = "D2691EFF" +option tfree_color : string = "A020F0FF" for color_dialog +option tvar_color : string = "A020F0FF" for color_dialog +option free_color : string = "0000FFFF" for color_dialog +option skolem_color : string = "D2691EFF" for color_dialog +option bound_color : string = "008000FF" for color_dialog +option var_color : string = "00009BFF" for color_dialog +option inner_numeral_color : string = "FF0000FF" for color_dialog +option inner_quoted_color : string = "FF00CCFF" for color_dialog +option inner_cartouche_color : string = "CC6600FF" for color_dialog +option dynamic_color : string = "7BA428FF" for color_dialog +option class_parameter_color : string = "D2691EFF" for color_dialog -option markdown_bullet1_color : string = "DAFEDAFF" -option markdown_bullet2_color : string = "FFF0CCFF" -option markdown_bullet3_color : string = "E7E7FFFF" -option markdown_bullet4_color : string = "FFE0F0FF" +option markdown_bullet1_color : string = "DAFEDAFF" for color_dialog +option markdown_bullet2_color : string = "FFF0CCFF" for color_dialog +option markdown_bullet3_color : string = "E7E7FFFF" for color_dialog +option markdown_bullet4_color : string = "FFE0F0FF" for color_dialog section "Icons"