# HG changeset patch
# User wenzelm
# Date 1488574612 -3600
# Node ID 27d376c33c021a621c8076938f9ad5f9ce113ac2
# Parent  eb21a4f70b0ee24c831e018d3158d49cb29bc279
tuned;

diff -r eb21a4f70b0e -r 27d376c33c02 src/Tools/VSCode/extension/src/extension.ts
--- 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());
   }