tuned;
authorwenzelm
Tue Mar 07 17:21:41 2017 +0100 (2017-03-07)
changeset 6514336cd85caf09a
parent 65142 368004bed323
child 65144 b5782e996651
tuned;
src/Pure/PIDE/rendering.scala
src/Tools/VSCode/src/vscode_rendering.scala
     1.1 --- a/src/Pure/PIDE/rendering.scala	Tue Mar 07 16:06:42 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Tue Mar 07 17:21:41 2017 +0100
     1.3 @@ -26,12 +26,12 @@
     1.4      val markdown_item2 = Value("markdown_item2")
     1.5      val markdown_item3 = Value("markdown_item3")
     1.6      val markdown_item4 = Value("markdown_item4")
     1.7 -    val background = values
     1.8 +    val background_colors = values
     1.9  
    1.10      // foreground
    1.11      val quoted = Value("quoted")
    1.12      val antiquoted = Value("antiquoted")
    1.13 -    val foreground = values -- background
    1.14 +    val foreground_colors = values -- background_colors
    1.15  
    1.16      // message underline
    1.17      val writeln = Value("writeln")
    1.18 @@ -39,7 +39,7 @@
    1.19      val warning = Value("warning")
    1.20      val legacy = Value("legacy")
    1.21      val error = Value("error")
    1.22 -    val message_underline = values -- background -- foreground
    1.23 +    val message_underline_colors = values -- background_colors -- foreground_colors
    1.24  
    1.25      // message background
    1.26      val writeln_message = Value("writeln_message")
    1.27 @@ -48,7 +48,8 @@
    1.28      val warning_message = Value("warning_message")
    1.29      val legacy_message = Value("legacy_message")
    1.30      val error_message = Value("error_message")
    1.31 -    val message_background = values -- background -- foreground -- message_underline
    1.32 +    val message_background_colors =
    1.33 +      values -- background_colors -- foreground_colors -- message_underline_colors
    1.34    }
    1.35  
    1.36  
     2.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 16:06:42 2017 +0100
     2.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 17:21:41 2017 +0100
     2.3 @@ -135,9 +135,9 @@
     2.4    /* decorations */
     2.5  
     2.6    def decorations: List[Document_Model.Decoration] = // list of canonical length and order
     2.7 -    VSCode_Rendering.color_decorations("background_", Rendering.Color.background,
     2.8 +    VSCode_Rendering.color_decorations("background_", Rendering.Color.background_colors,
     2.9        background(model.content.text_range, Set.empty)) :::
    2.10 -    VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground,
    2.11 +    VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
    2.12        foreground(model.content.text_range)) :::
    2.13      VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
    2.14        dotted(model.content.text_range)) :::