avoid hard-wired stuff (see also 78f2475aa126);
authorwenzelm
Sat, 11 Mar 2023 13:31:16 +0100
changeset 77612 3e235fab64db
parent 77611 606ac3fae270
child 77613 44f7b76d1106
avoid hard-wired stuff (see also 78f2475aa126);
src/Pure/System/options.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/jedit_options.scala
--- a/src/Pure/System/options.scala	Sat Mar 11 12:48:37 2023 +0100
+++ b/src/Pure/System/options.scala	Sat Mar 11 13:31:16 2023 +0100
@@ -48,6 +48,7 @@
   val TAG_BUILD = "build"        // relavant for "isabelle build"
   val TAG_UPDATE = "update"      // relevant for "isabelle update"
   val TAG_CONNECTION = "connection"  // private information about connections (password etc.)
+  val TAG_COLOR_DIALOG = "color_dialog"  // special color selection dialog
 
   case class Entry(
     public: Boolean,
@@ -91,8 +92,8 @@
     def unknown: Boolean = typ == Unknown
 
     def has_tag(tag: String): Boolean = tags.contains(tag)
-
     def session_content: Boolean = has_tag(TAG_CONTENT) || has_tag(TAG_DOCUMENT)
+    def color_dialog: Boolean = has_tag(TAG_COLOR_DIALOG)
   }
 
 
--- 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"
--- a/src/Tools/jEdit/src/jedit_options.scala	Sat Mar 11 12:48:37 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat Mar 11 13:31:16 2023 +0100
@@ -122,7 +122,7 @@
     private val predefined =
       (for {
         opt <- PIDE.options.value.iterator
-        if opt.name.endsWith("_color") && opt.section == "Rendering of Document Content"
+        if opt.color_dialog
       } yield PIDE.options.make_color_component(opt)).toList
 
     assert(predefined.nonEmpty)