src/Pure/PIDE/rendering.scala
changeset 65143 36cd85caf09a
parent 65139 0a2c0712e432
child 65144 b5782e996651
     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