decorations for background and foreground colors;

--- 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
   }
 
 

--- a/src/Tools/VSCode/extension/package.json	Sat Mar 04 13:33:47 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json	Sat Mar 04 13:36:06 2017 +0100
@@ -67,7 +67,33 @@
                     "items": { "type": "string" },
                     "default": [],
                     "description": "Command-line arguments for isabelle vscode_server process."
-                }
+                },
+                "isabelle.unprocessed1_light_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" },
+                "isabelle.unprocessed1_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" },
+                "isabelle.running1_light_color": { "type": "string", "default": "rgba(97, 0, 97, 0.39)" },
+                "isabelle.running1_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 0.39)" },
+                "isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.39)" },
+                "isabelle.bad_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.39)" },
+                "isabelle.intensify_light_color": { "type": "string", "default": "rgba(255, 204, 102, 0.39)" },
+                "isabelle.intensify_dark_color": { "type": "string", "default": "rgba(255, 204, 102, 0.39)" },
+                "isabelle.entity_light_color": { "type": "string", "default": "rgba(204, 217, 255, 0.50)" },
+                "isabelle.entity_dark_color": { "type": "string", "default": "rgba(204, 217, 255, 0.50)" },
+                "isabelle.active_light_color": { "type": "string", "default": "rgba(220, 220, 220, 1.00)" },
+                "isabelle.active_dark_color": { "type": "string", "default": "rgba(220, 220, 220, 1.00)" },
+                "isabelle.active_result_light_color": { "type": "string", "default": "rgba(153, 153, 102, 1.00)" },
+                "isabelle.active_result_dark_color": { "type": "string", "default": "rgba(153, 153, 102, 1.00)" },
+                "isabelle.markdown_item1_light_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" },
+                "isabelle.markdown_item1_dark_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" },
+                "isabelle.markdown_item2_light_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" },
+                "isabelle.markdown_item2_dark_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" },
+                "isabelle.markdown_item3_light_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" },
+                "isabelle.markdown_item3_dark_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" },
+                "isabelle.markdown_item4_light_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" },
+                "isabelle.markdown_item4_dark_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" },
+                "isabelle.quoted_light_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" },
+                "isabelle.quoted_dark_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" },
+                "isabelle.antiquoted_light_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" },
+                "isabelle.antiquoted_dark_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" }
             }
         }
     },

--- a/src/Tools/VSCode/extension/src/decorations.ts	Sat Mar 04 13:33:47 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Sat Mar 04 13:36:06 2017 +0100
@@ -7,13 +7,36 @@
 
 /* known decoration types */
 
-export interface Decorations
+export const types = new Map<string, TextEditorDecorationType>()
+
+const background_colors = [
+  "unprocessed1",
+  "running1",
+  "bad",
+  "intensify",
+  "entity",
+  "quoted",
+  "antiquoted",
+  "active",
+  "active_result",
+  "markdown_item1",
+  "markdown_item2",
+  "markdown_item3",
+  "markdown_item4"
+]
+
+const foreground_colors = [
+  "quoted",
+  "antiquoted"
+]
+
+function property(prop: string, config: string): Object
 {
-  bad: TextEditorDecorationType
+  let res = {}
+  res[prop] = vscode.workspace.getConfiguration("isabelle").get<string>(config)
+  return res
 }
 
-export let types: Decorations
-
 export function init(context: ExtensionContext)
 {
   function decoration(options: DecorationRenderOptions): TextEditorDecorationType
@@ -23,11 +46,22 @@
     return typ
   }
 
-  if (!types)
-    types =
-    {
-      bad: decoration({ backgroundColor: 'rgba(255, 106, 106, 0.4)' })
-    }
+  function background(color: string): TextEditorDecorationType
+  {
+    const prop = "backgroundColor"
+    const light = property(prop, color.concat("_light_color"))
+    const dark = property(prop, color.concat("_dark_color"))
+    return decoration({ light: light, dark: dark })
+  }
+
+  types.clear
+  for (let color of background_colors) {
+    types["background_".concat(color)] = background(color)
+  }
+  for (let color of foreground_colors) {
+    types["foreground_".concat(color)] = background(color) // approximation
+  }
+  types["bad"] = decoration({})
 }
 
 

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sat Mar 04 13:33:47 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sat Mar 04 13:36:06 2017 +0100
@@ -15,6 +15,25 @@
 
 object VSCode_Rendering
 {
+  /* decorations */
+
+  def color_decorations(prefix: String, types: Rendering.Color.ValueSet,
+    colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] =
+  {
+    val color_ranges =
+      (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) {
+        case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil)))
+      }
+    for (c <- types.toList)
+    yield {
+      val typ = prefix + c.toString
+      val content =
+        color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: XML.Body))
+      Document_Model.Decoration(typ, content)
+    }
+  }
+
+
   /* diagnostic messages */
 
   private val message_severity =
@@ -97,13 +116,21 @@
   /* decorations */
 
   def decorations: List[Document_Model.Decoration] =
-    List(Document_Model.Decoration(Protocol.Decorations.bad, decorations_bad))
+    decorations_bad :::
+    VSCode_Rendering.color_decorations("background_", Rendering.Color.background,
+      background(model.content.text_range, Set.empty)) :::
+    VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground,
+      foreground(model.content.text_range))
 
-  def decorations_bad: List[Text.Info[XML.Body]] =
-    snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ =>
-      {
-        case Text.Info(_, XML.Elem(_, body)) => Some(body)
-      })
+  def decorations_bad: List[Document_Model.Decoration] =
+  {
+    val content =
+      snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ =>
+        {
+          case Text.Info(_, XML.Elem(_, body)) => Some(body)
+        })
+    List(Document_Model.Decoration(Protocol.Decorations.bad, content))
+  }
 
   def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
   {