--- 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)) :::