src/Tools/VSCode/extension/src/decorations.ts

--- a/src/Tools/VSCode/extension/src/decorations.ts	Sun Mar 05 22:06:13 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Sun Mar 05 22:32:33 2017 +0100
@@ -30,11 +30,15 @@
   "antiquoted"
 ]
 
-function property(prop: string, config: string): Object
+const dotted_colors = [
+  "writeln",
+  "information"
+]
+
+function get_color(color: string, light: boolean): string
 {
-  let res = {}
-  res[prop] = vscode.workspace.getConfiguration("isabelle").get<string>(config)
-  return res
+  const config = color.concat(light ? "_light" : "_dark").concat("_color")
+  return vscode.workspace.getConfiguration("isabelle").get<string>(config)
 }
 
 export function init(context: ExtensionContext)
@@ -48,10 +52,17 @@
 
   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 })
+    return decoration(
+      { light: { backgroundColor: get_color(color, true) },
+        dark: { backgroundColor: get_color(color, false) } })
+  }
+
+  function dotted(color: string): TextEditorDecorationType
+  {
+    const border = "2px none; border-bottom-style: dotted; border-color: "
+    return decoration(
+      { light: { border: border.concat(get_color(color, true)) },
+        dark: { border: border.concat(get_color(color, false)) } })
   }
 
   types.clear
@@ -61,6 +72,9 @@
   for (let color of foreground_colors) {
     types["foreground_".concat(color)] = background(color) // approximation
   }
+  for (let color of dotted_colors) {
+    types["dotted_".concat(color)] = dotted(color)
+  }
   types["hover_message"] = decoration({})
 }