# HG changeset patch
# User wenzelm
# Date 1497127840 -7200
# Node ID a2e441805d6a1408d80ad8eb87acc4ac7e9c771a
# Parent  175772371cd015b8d22cfb11b6ba1f7c88e2db8c
superseded by external protocol;

diff -r 175772371cd0 -r a2e441805d6a src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Sat Jun 10 22:48:35 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sat Jun 10 22:50:40 2017 +0200
@@ -123,13 +123,14 @@
 
 
     /* completion */
+/* FIXME unused
 
     const completion_provider = new completion.Completion_Provider
     for (const mode of ["isabelle", "isabelle-ml"]) {
       context.subscriptions.push(
         languages.registerCompletionItemProvider(mode, completion_provider))
     }
-
+*/
 
     /* start server */