--- a/src/Tools/VSCode/extension/src/extension.ts Fri Mar 03 21:51:04 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts Fri Mar 03 21:56:52 2017 +0100
@@ -39,8 +39,7 @@
let client = new LanguageClient("Isabelle", server_options, client_options, false)
decorations.init(context)
- client.onNotification<Decoration>({method: "PIDE/decoration"},
- function (decoration: Decoration) { return decorations.apply(decoration) })
+ client.onNotification<Decoration>({method: "PIDE/decoration"}, decorations.apply)
context.subscriptions.push(client.start());
}