--- a/src/Pure/PIDE/rendering.scala Sat Mar 04 13:33:47 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala Sat Mar 04 13:36:06 2017 +0100
@@ -14,19 +14,24 @@
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 quoted = Value("quoted")
- val antiquoted = Value("antiquoted")
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 background = values
+
+ // foreground
+ val quoted = Value("quoted")
+ val antiquoted = Value("antiquoted")
+ val foreground = values -- background
}