superseded by external protocol;

--- 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 */