# HG changeset patch
# User wenzelm
# Date 1488903701 -3600
# Node ID 36cd85caf09a219ff70f5e6100287843aa00eb97
# Parent  368004bed323f006a35cc8d5a722283f39e4b3b8
tuned;

diff -r 368004bed323 -r 36cd85caf09a src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Tue Mar 07 16:06:42 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Tue Mar 07 17:21:41 2017 +0100
@@ -26,12 +26,12 @@
     val markdown_item2 = Value("markdown_item2")
     val markdown_item3 = Value("markdown_item3")
     val markdown_item4 = Value("markdown_item4")
-    val background = values
+    val background_colors = values
 
     // foreground
     val quoted = Value("quoted")
     val antiquoted = Value("antiquoted")
-    val foreground = values -- background
+    val foreground_colors = values -- background_colors
 
     // message underline
     val writeln = Value("writeln")
@@ -39,7 +39,7 @@
     val warning = Value("warning")
     val legacy = Value("legacy")
     val error = Value("error")
-    val message_underline = values -- background -- foreground
+    val message_underline_colors = values -- background_colors -- foreground_colors
 
     // message background
     val writeln_message = Value("writeln_message")
@@ -48,7 +48,8 @@
     val warning_message = Value("warning_message")
     val legacy_message = Value("legacy_message")
     val error_message = Value("error_message")
-    val message_background = values -- background -- foreground -- message_underline
+    val message_background_colors =
+      values -- background_colors -- foreground_colors -- message_underline_colors
   }
 
 
diff -r 368004bed323 -r 36cd85caf09a src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 16:06:42 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 17:21:41 2017 +0100
@@ -135,9 +135,9 @@
   /* decorations */
 
   def decorations: List[Document_Model.Decoration] = // list of canonical length and order
-    VSCode_Rendering.color_decorations("background_", Rendering.Color.background,
+    VSCode_Rendering.color_decorations("background_", Rendering.Color.background_colors,
       background(model.content.text_range, Set.empty)) :::
-    VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground,
+    VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
       foreground(model.content.text_range)) :::
     VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
       dotted(model.content.text_range)) :::