src/Tools/jEdit/src/jedit_rendering.scala
changeset 65102 136b620b11af
parent 65101 4263b2a201b3
child 65121 12c6774a8f65
equal deleted inserted replaced
65101:4263b2a201b3 65102:136b620b11af
   164 class JEdit_Rendering(snapshot: Document.Snapshot, options: Options)
   164 class JEdit_Rendering(snapshot: Document.Snapshot, options: Options)
   165   extends Rendering(snapshot, options, PIDE.resources)
   165   extends Rendering(snapshot, options, PIDE.resources)
   166 {
   166 {
   167   /* colors */
   167   /* colors */
   168 
   168 
   169   def color_value(s: String): Color = Color_Value(options.string(s))
   169   def color(s: String): Color = Color_Value(options.string(s))
   170 
   170 
   171   lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
   171   lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
   172     Rendering.Color.values.iterator.map(c => c -> color_value(c.toString + "_color")).toMap
   172     Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap
   173 
   173 
   174   def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
   174   def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
   175 
   175 
   176   val outdated_color = color_value("outdated_color")
   176   val outdated_color = color("outdated_color")
   177   val unprocessed_color = color_value("unprocessed_color")
   177   val unprocessed_color = color("unprocessed_color")
   178   val running_color = color_value("running_color")
   178   val running_color = color("running_color")
   179   val bullet_color = color_value("bullet_color")
   179   val bullet_color = color("bullet_color")
   180   val tooltip_color = color_value("tooltip_color")
   180   val tooltip_color = color("tooltip_color")
   181   val writeln_color = color_value("writeln_color")
   181   val writeln_color = color("writeln_color")
   182   val information_color = color_value("information_color")
   182   val information_color = color("information_color")
   183   val warning_color = color_value("warning_color")
   183   val warning_color = color("warning_color")
   184   val legacy_color = color_value("legacy_color")
   184   val legacy_color = color("legacy_color")
   185   val error_color = color_value("error_color")
   185   val error_color = color("error_color")
   186   val writeln_message_color = color_value("writeln_message_color")
   186   val writeln_message_color = color("writeln_message_color")
   187   val information_message_color = color_value("information_message_color")
   187   val information_message_color = color("information_message_color")
   188   val tracing_message_color = color_value("tracing_message_color")
   188   val tracing_message_color = color("tracing_message_color")
   189   val warning_message_color = color_value("warning_message_color")
   189   val warning_message_color = color("warning_message_color")
   190   val legacy_message_color = color_value("legacy_message_color")
   190   val legacy_message_color = color("legacy_message_color")
   191   val error_message_color = color_value("error_message_color")
   191   val error_message_color = color("error_message_color")
   192   val spell_checker_color = color_value("spell_checker_color")
   192   val spell_checker_color = color("spell_checker_color")
   193   val entity_ref_color = color_value("entity_ref_color")
   193   val entity_ref_color = color("entity_ref_color")
   194   val breakpoint_disabled_color = color_value("breakpoint_disabled_color")
   194   val breakpoint_disabled_color = color("breakpoint_disabled_color")
   195   val breakpoint_enabled_color = color_value("breakpoint_enabled_color")
   195   val breakpoint_enabled_color = color("breakpoint_enabled_color")
   196   val caret_debugger_color = color_value("caret_debugger_color")
   196   val caret_debugger_color = color("caret_debugger_color")
   197   val antiquote_color = color_value("antiquote_color")
   197   val antiquote_color = color("antiquote_color")
   198   val highlight_color = color_value("highlight_color")
   198   val highlight_color = color("highlight_color")
   199   val hyperlink_color = color_value("hyperlink_color")
   199   val hyperlink_color = color("hyperlink_color")
   200   val active_hover_color = color_value("active_hover_color")
   200   val active_hover_color = color("active_hover_color")
   201   val keyword1_color = color_value("keyword1_color")
   201   val keyword1_color = color("keyword1_color")
   202   val keyword2_color = color_value("keyword2_color")
   202   val keyword2_color = color("keyword2_color")
   203   val keyword3_color = color_value("keyword3_color")
   203   val keyword3_color = color("keyword3_color")
   204   val quasi_keyword_color = color_value("quasi_keyword_color")
   204   val quasi_keyword_color = color("quasi_keyword_color")
   205   val improper_color = color_value("improper_color")
   205   val improper_color = color("improper_color")
   206   val operator_color = color_value("operator_color")
   206   val operator_color = color("operator_color")
   207   val caret_invisible_color = color_value("caret_invisible_color")
   207   val caret_invisible_color = color("caret_invisible_color")
   208   val completion_color = color_value("completion_color")
   208   val completion_color = color("completion_color")
   209   val search_color = color_value("search_color")
   209   val search_color = color("search_color")
   210 
   210 
   211   val tfree_color = color_value("tfree_color")
   211   val tfree_color = color("tfree_color")
   212   val tvar_color = color_value("tvar_color")
   212   val tvar_color = color("tvar_color")
   213   val free_color = color_value("free_color")
   213   val free_color = color("free_color")
   214   val skolem_color = color_value("skolem_color")
   214   val skolem_color = color("skolem_color")
   215   val bound_color = color_value("bound_color")
   215   val bound_color = color("bound_color")
   216   val var_color = color_value("var_color")
   216   val var_color = color("var_color")
   217   val inner_numeral_color = color_value("inner_numeral_color")
   217   val inner_numeral_color = color("inner_numeral_color")
   218   val inner_quoted_color = color_value("inner_quoted_color")
   218   val inner_quoted_color = color("inner_quoted_color")
   219   val inner_cartouche_color = color_value("inner_cartouche_color")
   219   val inner_cartouche_color = color("inner_cartouche_color")
   220   val inner_comment_color = color_value("inner_comment_color")
   220   val inner_comment_color = color("inner_comment_color")
   221   val dynamic_color = color_value("dynamic_color")
   221   val dynamic_color = color("dynamic_color")
   222   val class_parameter_color = color_value("class_parameter_color")
   222   val class_parameter_color = color("class_parameter_color")
   223 
   223 
   224 
   224 
   225   /* indentation */
   225   /* indentation */
   226 
   226 
   227   def indentation(range: Text.Range): Int =
   227   def indentation(range: Text.Range): Int =