# HG changeset patch
# User wenzelm
# Date 1489237426 -3600
# Node ID 973b7669e7d9ad02f5ceba24d7244bc3a41d522b
# Parent  b4105202751cd1ac8a40c93aa15c3c98be02705e
proper Map operations;
re-init decorations after configuration change;

diff -r b4105202751c -r 973b7669e7d9 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Sat Mar 11 12:24:54 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Sat Mar 11 14:03:46 2017 +0100
@@ -8,8 +8,6 @@
 
 /* known decoration types */
 
-export const types = new Map<string, TextEditorDecorationType>()
-
 const background_colors = [
   "unprocessed1",
   "running1",
@@ -57,6 +55,11 @@
   "antiquote"
 ]
 
+
+/* init */
+
+const types = new Map<string, TextEditorDecorationType>()
+
 export function init(context: ExtensionContext)
 {
   function decoration(options: DecorationRenderOptions): TextEditorDecorationType
@@ -88,20 +91,43 @@
         dark: { border: border + get_color(color, false) } })
   }
 
-  types.clear
+
+  /* reset */
+
+  types.forEach(typ =>
+  {
+    for (const editor of vscode.window.visibleTextEditors) {
+      editor.setDecorations(typ, [])
+    }
+    const i = context.subscriptions.indexOf(typ)
+    if (i >= 0) context.subscriptions.splice(i, 1)
+    typ.dispose()
+  })
+  types.clear()
+
+
+  /* init */
+
   for (const color of background_colors) {
-    types["background_" + color] = background(color)
+    types.set("background_" + color, background(color))
   }
   for (const color of foreground_colors) {
-    types["foreground_" + color] = background(color) // approximation
+    types.set("foreground_" + color, background(color)) // approximation
   }
   for (const color of dotted_colors) {
-    types["dotted_" + color] = bottom_border("2px", "dotted", color)
+    types.set("dotted_" + color, bottom_border("2px", "dotted", color))
   }
   for (const color of text_colors) {
-    types["text_" + color] = text_color(color)
+    types.set("text_" + color, text_color(color))
   }
-  types["spell_checker"] = bottom_border("1px", "solid", "spell_checker")
+  types.set("spell_checker", bottom_border("1px", "solid", "spell_checker"))
+
+
+  /* update editors */
+
+  for (const editor of vscode.window.visibleTextEditors) {
+    update_editor(editor)
+  }
 }
 
 
@@ -129,7 +155,7 @@
 
 export function apply_decoration(decoration: Decoration)
 {
-  const typ = types[decoration.type]
+  const typ = types.get(decoration.type)
   if (typ) {
     const uri = Uri.parse(decoration.uri).toString()
     const content: DecorationOptions[] = decoration.content.map(opt =>
@@ -159,7 +185,7 @@
     const decorations = document_decorations.get(editor.document.uri.toString())
     if (decorations) {
       for (const [typ, content] of decorations) {
-        editor.setDecorations(types[typ], content)
+        editor.setDecorations(types.get(typ), content)
       }
     }
   }
diff -r b4105202751c -r 973b7669e7d9 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Sat Mar 11 12:24:54 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sat Mar 11 14:03:46 2017 +0100
@@ -35,6 +35,9 @@
   const isabelle_args = get_configuration().get<Array<string>>("args")
   const cygwin_root = get_configuration().get<string>("cygwin_root")
 
+
+  /* server */
+
   if (isabelle_home === "")
     vscode.window.showErrorMessage("Missing user settings: isabelle.home")
   else {
@@ -55,13 +58,21 @@
 
     const client = new LanguageClient("Isabelle", server_options, client_options, false)
 
+
+    /* decorations */
+
     decorations.init(context)
+    vscode.workspace.onDidChangeConfiguration(() => decorations.init(context))
     vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)
     vscode.workspace.onDidCloseTextDocument(decorations.close_document)
+
     client.onReady().then(() =>
       client.onNotification(
         new NotificationType<Decoration, void>("PIDE/decoration"), decorations.apply_decoration))
 
+
+    /* start server */
+
     context.subscriptions.push(client.start());
   }
 }