# HG changeset patch
# User wenzelm
# Date 1493490613 -7200
# Node ID e9b87bf6578b76e04b87d7407f05cecc9c9bcc7a
# Parent  df804cdba5f93992923f08bf2fc77482d984bb32
tuned;

diff -r df804cdba5f9 -r e9b87bf6578b src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sat Apr 29 20:15:26 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala	Sat Apr 29 20:30:13 2017 +0200
@@ -15,63 +15,28 @@
   object Color extends Enumeration
   {
     // background
-    val unprocessed1 = Value("unprocessed1")
-    val running1 = Value("running1")
-    val bad = Value("bad")
-    val intensify = Value("intensify")
-    val entity = Value("entity")
-    val active = Value("active")
-    val active_result = Value("active_result")
-    val markdown_item1 = Value("markdown_item1")
-    val markdown_item2 = Value("markdown_item2")
-    val markdown_item3 = Value("markdown_item3")
-    val markdown_item4 = Value("markdown_item4")
+    val unprocessed1, running1, bad, intensify, entity, active, active_result,
+      markdown_item1, markdown_item2, markdown_item3, markdown_item4 = Value
     val background_colors = values
 
     // foreground
-    val quoted = Value("quoted")
-    val antiquoted = Value("antiquoted")
+    val quoted, antiquoted = Value
     val foreground_colors = values -- background_colors
 
     // message underline
-    val writeln = Value("writeln")
-    val information = Value("information")
-    val warning = Value("warning")
-    val legacy = Value("legacy")
-    val error = Value("error")
+    val writeln, information, warning, legacy, error = Value
     val message_underline_colors = values -- background_colors -- foreground_colors
 
     // message background
-    val writeln_message = Value("writeln_message")
-    val information_message = Value("information_message")
-    val tracing_message = Value("tracing_message")
-    val warning_message = Value("warning_message")
-    val legacy_message = Value("legacy_message")
-    val error_message = Value("error_message")
+    val writeln_message, information_message, tracing_message,
+      warning_message, legacy_message, error_message = Value
     val message_background_colors =
       values -- background_colors -- foreground_colors -- message_underline_colors
 
     // text
-    val main = Value("main")
-    val keyword1 = Value("keyword1")
-    val keyword2 = Value("keyword2")
-    val keyword3 = Value("keyword3")
-    val quasi_keyword = Value("quasi_keyword")
-    val improper = Value("improper")
-    val operator = Value("operator")
-    val tfree = Value("tfree")
-    val tvar = Value("tvar")
-    val free = Value("free")
-    val skolem = Value("skolem")
-    val bound = Value("bound")
-    val var_ = Value("var")
-    val inner_numeral = Value("inner_numeral")
-    val inner_quoted = Value("inner_quoted")
-    val inner_cartouche = Value("inner_cartouche")
-    val inner_comment = Value("inner_comment")
-    val dynamic = Value("dynamic")
-    val class_parameter = Value("class_parameter")
-    val antiquote = Value("antiquote")
+    val main, keyword1, keyword2, keyword3, quasi_keyword, improper, operator,
+      tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted,
+      inner_cartouche, inner_comment, dynamic, class_parameter, antiquote = Value
     val text_colors =
       values -- background_colors -- foreground_colors -- message_underline_colors --
       message_background_colors
@@ -149,7 +114,7 @@
     Markup.FREE -> Color.free,
     Markup.SKOLEM -> Color.skolem,
     Markup.BOUND -> Color.bound,
-    Markup.VAR -> Color.var_,
+    Markup.VAR -> Color.`var`,
     Markup.INNER_STRING -> Color.inner_quoted,
     Markup.INNER_CARTOUCHE -> Color.inner_cartouche,
     Markup.INNER_COMMENT -> Color.inner_comment,