# HG changeset patch
# User wenzelm
# Date 1488616164 -3600
# Node ID 136b620b11afae64752aeb38a3205a49f9e1c8a2
# Parent  4263b2a201b3165e98186a1a4384124875b8fe71
tuned signature;

diff -r 4263b2a201b3 -r 136b620b11af src/Tools/jEdit/src/jedit_rendering.scala
--- 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 */