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());
   }