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