# HG changeset patch
# User wenzelm
# Date 1489091101 -3600
# Node ID 9eabc312a2a2e9b8e811d2037d8c7aedca428d9a
# Parent  ee569aac344b77b4367f528c5c1ead534ed8b37a
prefer immutable bindings;

diff -r ee569aac344b -r 9eabc312a2a2 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Thu Mar 09 21:22:01 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Thu Mar 09 21:25:01 2017 +0100
@@ -96,16 +96,16 @@
   }
 
   types.clear
-  for (let color of background_colors) {
+  for (const color of background_colors) {
     types["background_" + color] = background(color)
   }
-  for (let color of foreground_colors) {
+  for (const color of foreground_colors) {
     types["foreground_" + color] = background(color) // approximation
   }
-  for (let color of dotted_colors) {
+  for (const color of dotted_colors) {
     types["dotted_" + color] = bottom_border("2px", "dotted", color)
   }
-  for (let color of text_colors) {
+  for (const color of text_colors) {
     types["text_" + color] = text_color(color)
   }
   types["spell_checker"] = bottom_border("1px", "solid", "spell_checker")
@@ -140,11 +140,11 @@
       content: decoration0.content
     }
 
-    let document = document_decorations.get(decoration.uri) || new Map<string, Content>()
+    const 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) {
+    for (const editor of vscode.window.visibleTextEditors) {
       if (decoration.uri == editor.document.uri.toString()) {
         editor.setDecorations(typ, decoration.content)
       }
@@ -155,9 +155,9 @@
 export function update_editor(editor: TextEditor)
 {
   if (editor) {
-    let decorations = document_decorations.get(editor.document.uri.toString())
+    const decorations = document_decorations.get(editor.document.uri.toString())
     if (decorations) {
-      for (let [typ, content] of decorations) {
+      for (const [typ, content] of decorations) {
         editor.setDecorations(types[typ], content)
       }
     }
diff -r ee569aac344b -r 9eabc312a2a2 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Thu Mar 09 21:22:01 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Thu Mar 09 21:25:01 2017 +0100
@@ -11,31 +11,31 @@
 
 export function activate(context: vscode.ExtensionContext)
 {
-  let is_windows = os.type().startsWith("Windows")
+  const is_windows = os.type().startsWith("Windows")
 
-  let cygwin_root = vscode.workspace.getConfiguration("isabelle").get<string>("cygwin_root");
-  let isabelle_home = vscode.workspace.getConfiguration("isabelle").get<string>("home");
-  let isabelle_args = vscode.workspace.getConfiguration("isabelle").get<Array<string>>("args");
+  const cygwin_root = vscode.workspace.getConfiguration("isabelle").get<string>("cygwin_root");
+  const isabelle_home = vscode.workspace.getConfiguration("isabelle").get<string>("home");
+  const isabelle_args = vscode.workspace.getConfiguration("isabelle").get<Array<string>>("args");
 
   if (is_windows && cygwin_root == "")
     vscode.window.showErrorMessage("Missing user settings: isabelle.cygwin_root")
   else if (isabelle_home == "")
     vscode.window.showErrorMessage("Missing user settings: isabelle.home")
   else {
-    let isabelle_tool = isabelle_home + "/bin/isabelle"
-    let standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
+    const isabelle_tool = isabelle_home + "/bin/isabelle"
+    const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
 
-    let server_options: ServerOptions =
+    const server_options: ServerOptions =
       is_windows ?
         { command: cygwin_root + "/bin/bash",
           args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } :
         { command: isabelle_tool,
           args: ["vscode_server"].concat(standard_args, isabelle_args) };
-    let client_options: LanguageClientOptions = {
+    const client_options: LanguageClientOptions = {
       documentSelector: ["isabelle", "isabelle-ml", "bibtex"]
     };
 
-    let client = new LanguageClient("Isabelle", server_options, client_options, false)
+    const client = new LanguageClient("Isabelle", server_options, client_options, false)
 
     decorations.init(context)
     vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)