# HG changeset patch
# User wenzelm
# Date 1488841576 -3600
# Node ID 158cba86140f7f849ed94d91618da4e82c9aa2fa
# Parent  511bf19348d32f2a65d851e45eea10b1823c518c
maintain decorations for document (model) and update it for each editor (view);

diff -r 511bf19348d3 -r 158cba86140f src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Mon Mar 06 18:28:48 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Tue Mar 07 00:06:16 2017 +0100
@@ -2,7 +2,7 @@
 
 import * as vscode from 'vscode'
 import { Range, MarkedString, DecorationOptions, DecorationRenderOptions,
-  TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
+  TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
 
 
 /* known decoration types */
@@ -88,14 +88,45 @@
   content: DecorationOptions[]
 }
 
-export function apply(decoration: Decoration)
+type Content = Range[] | DecorationOptions[]
+const document_decorations = new Map<string, Map<string, Content>>()
+
+export function close_document(document: TextDocument)
 {
-  let typ = types[decoration.type]
+  document_decorations.delete(document.uri.toString())
+}
+
+export function apply_decoration(decoration0: Decoration)
+{
+  const typ = types[decoration0.type]
   if (typ) {
-    let uri = Uri.parse(decoration.uri).toString()
-    let editor =
-      vscode.window.visibleTextEditors.find(
-        function (editor) { return uri == editor.document.uri.toString() })
-    if (editor) editor.setDecorations(typ, decoration.content)
+    const decoration =
+    {
+      uri: Uri.parse(decoration0.uri).toString(),
+      "type": decoration0.type,
+      content: decoration0.content
+    }
+
+    let document = document_decorations.get(decoration.uri) || new Map<string, Content>()
+    document.set(decoration.type, decoration.content)
+    document_decorations.set(decoration.uri, document)
+
+    for (let editor of vscode.window.visibleTextEditors) {
+      if (decoration.uri == editor.document.uri.toString()) {
+        editor.setDecorations(typ, decoration.content)
+      }
+    }
   }
-}
\ No newline at end of file
+}
+
+export function update_editor(editor: TextEditor)
+{
+  if (editor) {
+    let decorations = document_decorations.get(editor.document.uri.toString())
+    if (decorations) {
+      for (let [typ, content] of decorations) {
+        editor.setDecorations(types[typ], content)
+      }
+    }
+  }
+}
diff -r 511bf19348d3 -r 158cba86140f src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Mon Mar 06 18:28:48 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue Mar 07 00:06:16 2017 +0100
@@ -39,7 +39,9 @@
     let client = new LanguageClient("Isabelle", server_options, client_options, false)
 
     decorations.init(context)
-    client.onNotification<Decoration>({method: "PIDE/decoration"}, decorations.apply)
+    vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)
+    vscode.workspace.onDidCloseTextDocument(decorations.close_document)
+    client.onNotification<Decoration>({method: "PIDE/decoration"}, decorations.apply_decoration)
 
     context.subscriptions.push(client.start());
   }