src/Tools/VSCode/extension/src/preview.ts

--- a/src/Tools/VSCode/extension/src/preview.ts	Tue May 30 15:30:00 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts	Tue May 30 19:19:39 2017 +0200
@@ -1,8 +1,8 @@
 'use strict';
 
-import { TextDocumentContentProvider, ExtensionContext, Event, EventEmitter, Uri, Position,
-  workspace, window, commands } from 'vscode'
-
+import * as timers from 'timers'
+import { TextDocument, TextEditor, TextDocumentContentProvider, ExtensionContext,
+  Event, EventEmitter, Uri, Position, workspace, window, commands } from 'vscode'
 import * as library from './library'
 
 
@@ -10,12 +10,12 @@
 
 const uri_scheme = 'isabelle-preview';
 
-export function encode_name(document_uri: Uri): Uri
+export function encode_preview(document_uri: Uri): Uri
 {
   return Uri.parse(uri_scheme + ":Preview?" + JSON.stringify([document_uri.toString()]))
 }
 
-export function decode_name(preview_uri: Uri): Uri
+export function decode_preview(preview_uri: Uri): Uri
 {
   const [name] = <[string]>JSON.parse(preview_uri.query)
   return Uri.parse(name)
@@ -26,25 +26,12 @@
   dispose() { }
 
   private emitter = new EventEmitter<Uri>()
-  private waiting: boolean = false;
-
+  public update(preview_uri: Uri) { this.emitter.fire(preview_uri) }
   get onDidChange(): Event<Uri> { return this.emitter.event }
 
-  public update(document_uri: Uri)
-  {
-    if (!this.waiting) {
-      this.waiting = true
-      setTimeout(() =>
-      {
-        this.waiting = false
-        this.emitter.fire(encode_name(document_uri))
-      }, 300)
-    }
-  }
-
   provideTextDocumentContent(preview_uri: Uri): string | Thenable<string>
   {
-    const document_uri = decode_name(preview_uri)
+    const document_uri = decode_preview(preview_uri)
     const editor =
       window.visibleTextEditors.find(editor =>
         document_uri.toString() === editor.document.uri.toString())
@@ -67,26 +54,44 @@
 
 /* init */
 
+let provider: Provider
+
 export function init(context: ExtensionContext)
 {
-  const provider = new Provider()
+  provider = new Provider()
   context.subscriptions.push(workspace.registerTextDocumentContentProvider(uri_scheme, provider))
   context.subscriptions.push(provider)
 
   context.subscriptions.push(
     commands.registerTextEditorCommand("isabelle.preview", editor =>
     {
-      const preview_uri = encode_name(editor.document.uri)
+      const preview_uri = encode_preview(editor.document.uri)
       return workspace.openTextDocument(preview_uri).then(doc =>
         commands.executeCommand("vscode.previewHtml", preview_uri,
           library.other_column(window.activeTextEditor), "Isabelle Preview"))
     }))
+}
 
-  context.subscriptions.push(
-    workspace.onDidChangeTextDocument(event =>
-    {
-      if (event.document.languageId === 'isabelle') {
-        provider.update(event.document.uri)
-      }
-    }))
+
+/* handle document changes */
+
+const touched_documents = new Set<TextDocument>()
+let touched_timer: NodeJS.Timer
+
+function update_touched_documents()
+{
+  if (provider) {
+    for (const document of touched_documents) {
+      provider.update(encode_preview(document.uri))
+    }
+  }
 }
+
+export function touch_document(document: TextDocument)
+{
+  if (library.is_file(document.uri) && document.languageId === 'isabelle') {
+    if (touched_timer) timers.clearTimeout(touched_timer)
+    touched_documents.add(document)
+    touched_timer = timers.setTimeout(update_touched_documents, 300)
+  }
+}