# HG changeset patch
# User wenzelm
# Date 1489509139 -3600
# Node ID e37209c0a42a628aeb9b7b34927efeb6b30c2a72
# Parent  ca571c8c0788a6763a39ec7c719da82bfc905a57
always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;

diff -r ca571c8c0788 -r e37209c0a42a src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Tue Mar 14 16:20:07 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Tue Mar 14 17:32:19 2017 +0100
@@ -1,5 +1,6 @@
 'use strict';
 
+import * as timers from 'timers';
 import * as vscode from 'vscode'
 import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
   TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
@@ -179,3 +180,29 @@
     }
   }
 }
+
+
+/* decorations vs. document changes */
+
+const touched_documents = new Set<TextDocument>()
+
+function update_touched_documents()
+{
+  const touched_editors: TextEditor[] = []
+  for (const editor of vscode.window.visibleTextEditors) {
+    if (touched_documents.has(editor.document)) {
+      touched_editors.push(editor)
+    }
+  }
+  touched_documents.clear
+  touched_editors.forEach(update_editor)
+}
+
+let touched_timer: NodeJS.Timer
+
+export function touch_document(document: TextDocument)
+{
+  if (touched_timer) timers.clearTimeout(touched_timer)
+  touched_documents.add(document)
+  touched_timer = timers.setTimeout(update_touched_documents, 1000)
+}
diff -r ca571c8c0788 -r e37209c0a42a src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Tue Mar 14 16:20:07 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue Mar 14 17:32:19 2017 +0100
@@ -64,6 +64,7 @@
 
     decorations.init(context)
     vscode.workspace.onDidChangeConfiguration(() => decorations.init(context))
+    vscode.workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document))
     vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)
     vscode.workspace.onDidCloseTextDocument(decorations.close_document)