# HG changeset patch
# User wenzelm
# Date 1489243007 -3600
# Node ID 4659e87c379569a0112647a9d01810860764eb5d
# Parent  663bb1614d2311d4c02303d04cedb1dc25137958
tuned;

diff -r 663bb1614d23 -r 4659e87c3795 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Sat Mar 11 14:33:37 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sat Mar 11 15:36:47 2017 +0100
@@ -6,22 +6,21 @@
 import * as os from 'os';
 import * as decorations from './decorations';
 import { Decoration } from './decorations'
-import { WorkspaceConfiguration} from 'vscode'
 import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
   from 'vscode-languageclient';
 
 
 /* Isabelle configuration */
 
-export function get_configuration(): WorkspaceConfiguration
+export function get_configuration<T>(name: string): T
 {
-  return vscode.workspace.getConfiguration("isabelle")
+  return vscode.workspace.getConfiguration("isabelle").get<T>(name)
 }
 
 export function get_color(color: string, light: boolean): string
 {
   const config = color + (light ? "_light" : "_dark") + "_color"
-  return get_configuration().get<string>(config)
+  return get_configuration<string>(config)
 }
 
 
@@ -31,9 +30,9 @@
 {
   const is_windows = os.type().startsWith("Windows")
 
-  const isabelle_home = get_configuration().get<string>("home")
-  const isabelle_args = get_configuration().get<Array<string>>("args")
-  const cygwin_root = get_configuration().get<string>("cygwin_root")
+  const isabelle_home = get_configuration<string>("home")
+  const isabelle_args = get_configuration<Array<string>>("args")
+  const cygwin_root = get_configuration<string>("cygwin_root")
 
 
   /* server */