src/Pure/PIDE/rendering.scala
changeset 65104 66b19d05dcee
parent 65101 4263b2a201b3
child 65107 70b0113fa4ef
--- 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
   }