--- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 04 09:27:51 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 04 09:29:24 2017 +0100
@@ -166,60 +166,60 @@
{
/* colors */
- def color_value(s: String): Color = Color_Value(options.string(s))
+ def color(s: String): Color = Color_Value(options.string(s))
lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
- Rendering.Color.values.iterator.map(c => c -> color_value(c.toString + "_color")).toMap
+ Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap
def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
- val outdated_color = color_value("outdated_color")
- val unprocessed_color = color_value("unprocessed_color")
- val running_color = color_value("running_color")
- val bullet_color = color_value("bullet_color")
- val tooltip_color = color_value("tooltip_color")
- val writeln_color = color_value("writeln_color")
- val information_color = color_value("information_color")
- val warning_color = color_value("warning_color")
- val legacy_color = color_value("legacy_color")
- val error_color = color_value("error_color")
- val writeln_message_color = color_value("writeln_message_color")
- val information_message_color = color_value("information_message_color")
- val tracing_message_color = color_value("tracing_message_color")
- val warning_message_color = color_value("warning_message_color")
- val legacy_message_color = color_value("legacy_message_color")
- val error_message_color = color_value("error_message_color")
- val spell_checker_color = color_value("spell_checker_color")
- val entity_ref_color = color_value("entity_ref_color")
- val breakpoint_disabled_color = color_value("breakpoint_disabled_color")
- val breakpoint_enabled_color = color_value("breakpoint_enabled_color")
- val caret_debugger_color = color_value("caret_debugger_color")
- val antiquote_color = color_value("antiquote_color")
- val highlight_color = color_value("highlight_color")
- val hyperlink_color = color_value("hyperlink_color")
- val active_hover_color = color_value("active_hover_color")
- val keyword1_color = color_value("keyword1_color")
- val keyword2_color = color_value("keyword2_color")
- val keyword3_color = color_value("keyword3_color")
- val quasi_keyword_color = color_value("quasi_keyword_color")
- val improper_color = color_value("improper_color")
- val operator_color = color_value("operator_color")
- val caret_invisible_color = color_value("caret_invisible_color")
- val completion_color = color_value("completion_color")
- val search_color = color_value("search_color")
+ val outdated_color = color("outdated_color")
+ val unprocessed_color = color("unprocessed_color")
+ val running_color = color("running_color")
+ val bullet_color = color("bullet_color")
+ val tooltip_color = color("tooltip_color")
+ val writeln_color = color("writeln_color")
+ val information_color = color("information_color")
+ val warning_color = color("warning_color")
+ val legacy_color = color("legacy_color")
+ val error_color = color("error_color")
+ val writeln_message_color = color("writeln_message_color")
+ val information_message_color = color("information_message_color")
+ val tracing_message_color = color("tracing_message_color")
+ val warning_message_color = color("warning_message_color")
+ val legacy_message_color = color("legacy_message_color")
+ val error_message_color = color("error_message_color")
+ val spell_checker_color = color("spell_checker_color")
+ val entity_ref_color = color("entity_ref_color")
+ val breakpoint_disabled_color = color("breakpoint_disabled_color")
+ val breakpoint_enabled_color = color("breakpoint_enabled_color")
+ val caret_debugger_color = color("caret_debugger_color")
+ val antiquote_color = color("antiquote_color")
+ val highlight_color = color("highlight_color")
+ val hyperlink_color = color("hyperlink_color")
+ val active_hover_color = color("active_hover_color")
+ val keyword1_color = color("keyword1_color")
+ val keyword2_color = color("keyword2_color")
+ val keyword3_color = color("keyword3_color")
+ val quasi_keyword_color = color("quasi_keyword_color")
+ val improper_color = color("improper_color")
+ val operator_color = color("operator_color")
+ val caret_invisible_color = color("caret_invisible_color")
+ val completion_color = color("completion_color")
+ val search_color = color("search_color")
- val tfree_color = color_value("tfree_color")
- val tvar_color = color_value("tvar_color")
- val free_color = color_value("free_color")
- val skolem_color = color_value("skolem_color")
- val bound_color = color_value("bound_color")
- val var_color = color_value("var_color")
- val inner_numeral_color = color_value("inner_numeral_color")
- val inner_quoted_color = color_value("inner_quoted_color")
- val inner_cartouche_color = color_value("inner_cartouche_color")
- val inner_comment_color = color_value("inner_comment_color")
- val dynamic_color = color_value("dynamic_color")
- val class_parameter_color = color_value("class_parameter_color")
+ val tfree_color = color("tfree_color")
+ val tvar_color = color("tvar_color")
+ val free_color = color("free_color")
+ val skolem_color = color("skolem_color")
+ val bound_color = color("bound_color")
+ val var_color = color("var_color")
+ val inner_numeral_color = color("inner_numeral_color")
+ val inner_quoted_color = color("inner_quoted_color")
+ val inner_cartouche_color = color("inner_cartouche_color")
+ val inner_comment_color = color("inner_comment_color")
+ val dynamic_color = color("dynamic_color")
+ val class_parameter_color = color("class_parameter_color")
/* indentation */