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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 03 19:33:52 2017 +0100
@@ -0,0 +1,52 @@
+'use strict';
+
+import * as vscode from 'vscode'
+import { Range, MarkedString, DecorationOptions, DecorationRenderOptions,
+  TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
+
+
+/* known decoration types */
+
+export interface Decorations
+{
+  test: TextEditorDecorationType
+}
+
+export let types: Readonly<Decorations>
+
+export function init(context: ExtensionContext)
+{
+  function decoration(options: DecorationRenderOptions): TextEditorDecorationType
+  {
+    const typ = vscode.window.createTextEditorDecorationType(options)
+    context.subscriptions.push(typ)
+    return typ
+  }
+
+  if (!types)
+    types =
+    {
+      test: decoration({ backgroundColor: 'rgba(255,0,0,0.3)' })
+    }
+}
+
+
+/* decoration for document node */
+
+export interface Decoration
+{
+  uri: string,
+  "type": string,
+  content: DecorationOptions[]
+}
+
+export function apply(decoration: Decoration)
+{
+  let typ = types[decoration.type]
+  if (typ) {
+    let editor =
+      vscode.window.visibleTextEditors.find(
+        function (editor) { return decoration.uri == editor.document.uri.toString() })
+    if (editor) editor.setDecorations(typ, decoration.content)
+  }
+}
\ No newline at end of file