# HG changeset patch
# User wenzelm
# Date 1488969941 -3600
# Node ID 82bd5d29adbf0f524c61353855a4301fe0a2098c
# Parent  a920012ae16a882c094ab590e208f4056a62b6ea
tuned;

diff -r a920012ae16a -r 82bd5d29adbf src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Wed Mar 08 11:30:13 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Wed Mar 08 11:45:41 2017 +0100
@@ -60,7 +60,7 @@
 
 function get_color(color: string, light: boolean): string
 {
-  const config = color.concat(light ? "_light" : "_dark").concat("_color")
+  const config = color + (light ? "_light" : "_dark") + "_color"
   return vscode.workspace.getConfiguration("isabelle").get<string>(config)
 }
 
@@ -91,22 +91,22 @@
   {
     const border = `${width} none; border-bottom-style: ${style}; border-color: `
     return decoration(
-      { light: { border: border.concat(get_color(color, true)) },
-        dark: { border: border.concat(get_color(color, false)) } })
+      { light: { border: border + get_color(color, true) },
+        dark: { border: border + get_color(color, false) } })
   }
 
   types.clear
   for (let color of background_colors) {
-    types["background_".concat(color)] = background(color)
+    types["background_" + color] = background(color)
   }
   for (let color of foreground_colors) {
-    types["foreground_".concat(color)] = background(color) // approximation
+    types["foreground_" + color] = background(color) // approximation
   }
   for (let color of dotted_colors) {
-    types["dotted_".concat(color)] = bottom_border("2px", "dotted", color)
+    types["dotted_" + color] = bottom_border("2px", "dotted", color)
   }
   for (let color of text_colors) {
-    types["text_".concat(color)] = text_color(color)
+    types["text_" + color] = text_color(color)
   }
   types["spell_checker"] = bottom_border("1px", "solid", "spell_checker")
 }
diff -r a920012ae16a -r 82bd5d29adbf src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Mar 08 11:30:13 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Mar 08 11:45:41 2017 +0100
@@ -22,11 +22,11 @@
   else if (isabelle_home == "")
     vscode.window.showErrorMessage("Missing user settings: isabelle.home")
   else {
-    let isabelle_tool = isabelle_home.concat("/bin/isabelle")
+    let isabelle_tool = isabelle_home + "/bin/isabelle"
     let standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
     let run =
       is_windows ?
-        { command: cygwin_root.concat("/bin/bash"),
+        { 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) };