# HG changeset patch
# User wenzelm
# Date 1488566032 -3600
# Node ID 386d9d487f62da8476384f1c842c85a5d315bf00
# Parent  5f08197206cefb1311093ceda236a63867fe9822
support for decorations;

diff -r 5f08197206ce -r 386d9d487f62 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
diff -r 5f08197206ce -r 386d9d487f62 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Fri Mar 03 17:53:24 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Fri Mar 03 19:33:52 2017 +0100
@@ -3,7 +3,8 @@
 import * as vscode from 'vscode';
 import * as path from 'path';
 import * as os from 'os';
-
+import * as decorations from './decorations';
+import { Decoration } from './decorations'
 import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind }
   from 'vscode-languageclient';
 
@@ -35,9 +36,14 @@
       documentSelector: ["isabelle", "isabelle-ml", "bibtex"]
     };
 
-    let disposable = new LanguageClient("Isabelle", server_options, client_options, false).start();
-    context.subscriptions.push(disposable);
-    }
+    let client = new LanguageClient("Isabelle", server_options, client_options, false)
+
+    decorations.init(context)
+    client.onNotification<Decoration>({method: "PIDE/decoration"},
+      function (decoration: Decoration) { return decorations.apply(decoration) })
+
+    context.subscriptions.push(client.start());
+  }
 }
 
 export function deactivate() { }
diff -r 5f08197206ce -r 386d9d487f62 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Fri Mar 03 17:53:24 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Fri Mar 03 19:33:52 2017 +0100
@@ -403,4 +403,22 @@
       Notification("textDocument/publishDiagnostics",
         Map("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json)))
   }
+
+
+  /* decorations */
+
+  sealed case class DecorationOptions(range: Line.Range, hover_message: List[MarkedString])
+  {
+    def json: JSON.T =
+      Map("range" -> Range(range)) ++
+      JSON.optional("hoverMessage" ->
+        (if (hover_message.isEmpty) None else Some(hover_message.map(_.json))))
+  }
+
+  object Decoration
+  {
+    def apply(file: JFile, typ: String, content: List[DecorationOptions]): JSON.T =
+      Notification("PIDE/decoration",
+        Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
+  }
 }