decorations for text color;

--- a/src/Tools/VSCode/extension/package.json	Tue Mar 07 18:12:59 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json	Tue Mar 07 18:50:42 2017 +0100
@@ -101,7 +101,45 @@
                 "isabelle.warning_light_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
                 "isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
                 "isabelle.spell_checker_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" },
-                "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" }
+                "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" },
+                "isabelle.keyword1_light_color": { "type": "string", "default": "rgba(0, 102, 153, 1.00)" },
+                "isabelle.keyword1_dark_color": { "type": "string", "default": "rgba(0, 102, 153, 1.00)" },
+                "isabelle.keyword2_light_color": { "type": "string", "default": "rgba(0, 153, 102, 1.00)" },
+                "isabelle.keyword2_dark_color": { "type": "string", "default": "rgba(0, 153, 102, 1.00)" },
+                "isabelle.keyword3_light_color": { "type": "string", "default": "rgba(0, 153, 255, 1.00)" },
+                "isabelle.keyword3_dark_color": { "type": "string", "default": "rgba(0, 153, 255, 1.00)" },
+                "isabelle.quasi_keyword_light_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" },
+                "isabelle.quasi_keyword_dark_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" },
+                "isabelle.improper_light_color": { "type": "string", "default": "rgba(255, 80, 80, 1.00)" },
+                "isabelle.improper_dark_color": { "type": "string", "default": "rgba(255, 80, 80, 1.00)" },
+                "isabelle.operator_light_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" },
+                "isabelle.operator_dark_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" },
+                "isabelle.tfree_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
+                "isabelle.tfree_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
+                "isabelle.tvar_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
+                "isabelle.tvar_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
+                "isabelle.free_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" },
+                "isabelle.free_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" },
+                "isabelle.skolem_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
+                "isabelle.skolem_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
+                "isabelle.bound_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" },
+                "isabelle.bound_dark_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" },
+                "isabelle.var_light_color": { "type": "string", "default": "rgba(0, 0, 155, 1.00)" },
+                "isabelle.var_dark_color": { "type": "string", "default": "rgba(0, 0, 155, 1.00)" },
+                "isabelle.inner_numeral_light_color": { "type": "string", "default": "rgba(255, 0, 0, 1.00)" },
+                "isabelle.inner_numeral_dark_color": { "type": "string", "default": "rgba(255, 0, 0, 1.00)" },
+                "isabelle.inner_quoted_light_color": { "type": "string", "default": "rgba(255, 0, 204, 1.00)" },
+                "isabelle.inner_quoted_dark_color": { "type": "string", "default": "rgba(255, 0, 204, 1.00)" },
+                "isabelle.inner_cartouche_light_color": { "type": "string", "default": "rgba(204, 102, 0, 1.00)" },
+                "isabelle.inner_cartouche_dark_color": { "type": "string", "default": "rgba(204, 102, 0, 1.00)" },
+                "isabelle.inner_comment_light_color": { "type": "string", "default": "rgba(204, 0, 0, 1.00)" },
+                "isabelle.inner_comment_dark_color": { "type": "string", "default": "rgba(204, 0, 0, 1.00)" },
+                "isabelle.dynamic_light_color": { "type": "string", "default": "rgba(123, 164, 40, 1.00)" },
+                "isabelle.dynamic_dark_color": { "type": "string", "default": "rgba(123, 164, 40, 1.00)" },
+                "isabelle.class_parameter_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
+                "isabelle.class_parameter_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
+                "isabelle.antiquote_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" },
+                "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" }
             }
         }
     },

--- a/src/Tools/VSCode/extension/src/decorations.ts	Tue Mar 07 18:12:59 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Tue Mar 07 18:50:42 2017 +0100
@@ -36,6 +36,28 @@
   "warning"
 ]
 
+const text_colors = [
+  "keyword1",
+  "keyword2",
+  "keyword3",
+  "quasi_keyword",
+  "improper",
+  "operator",
+  "tfree",
+  "tvar",
+  "free",
+  "skolem",
+  "bound",
+  "var",
+  "inner_numeral",
+  "inner_quoted",
+  "inner_cartouche",
+  "inner_comment",
+  "dynamic",
+  "class_parameter",
+  "antiquote"
+]
+
 function get_color(color: string, light: boolean): string
 {
   const config = color.concat(light ? "_light" : "_dark").concat("_color")
@@ -58,6 +80,13 @@
         dark: { backgroundColor: get_color(color, false) } })
   }
 
+  function text_color(color: string): TextEditorDecorationType
+  {
+    return decoration(
+      { light: { color: get_color(color, true) },
+        dark: { color: get_color(color, false) } })
+  }
+
   function bottom_border(width: string, style: string, color: string): TextEditorDecorationType
   {
     const border = `${width} none; border-bottom-style: ${style}; border-color: `
@@ -76,6 +105,9 @@
   for (let color of dotted_colors) {
     types["dotted_".concat(color)] = bottom_border("2px", "dotted", color)
   }
+  for (let color of text_colors) {
+    types["text_".concat(color)] = text_color(color)
+  }
   types["spell_checker"] = bottom_border("1px", "solid", "spell_checker")
 }
 

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 18:12:59 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 18:50:42 2017 +0100
@@ -111,6 +111,17 @@
   }
 
 
+  /* text color */
+
+  def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
+  {
+    snapshot.select(range, Rendering.text_color_elements, _ =>
+      {
+        case Text.Info(_, elem) => Rendering.text_color.get(elem.name)
+      })
+  }
+
+
   /* dotted underline */
 
   def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
@@ -139,6 +150,8 @@
       background(model.content.text_range, Set.empty)) :::
     VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
       foreground(model.content.text_range)) :::
+    VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors,
+      text_color(model.content.text_range)) :::
     VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
       dotted(model.content.text_range)) :::
     List(spell_checker)