# HG changeset patch
# User wenzelm
# Date 1497275569 -7200
# Node ID fd26cf23e9b2660d3239fd72cdebc93131a5beef
# Parent  8b67040b80cedd7fe4a8fcf10937c86280343bc0
retain vacuous CompletionProvider for now;

diff -r 8b67040b80ce -r fd26cf23e9b2 src/Tools/VSCode/extension/src/completion.ts
--- a/src/Tools/VSCode/extension/src/completion.ts	Mon Jun 12 15:44:08 2017 +0200
+++ b/src/Tools/VSCode/extension/src/completion.ts	Mon Jun 12 15:52:49 2017 +0200
@@ -11,26 +11,6 @@
   {
     const line_text = document.lineAt(position).text
 
-    let i = position.character
-    while (i > 0 && line_text.charAt(i - 1) !== "\\") { i = i - 1 }
-    const start = i - 1
-
-    let result = undefined as CompletionList
-    if (start >= 0 && line_text.charAt(start) == "\\") {
-      const s = line_text.substring(start + 1, position.character)
-      if (symbol.is_ascii_identifier(s)) {
-        const items =
-          symbol.complete_name(s).map((sym) =>
-          {
-            return {
-              label: sym,
-              detail: `(symbol ${symbol.get_unicode(sym)})`,
-              range: new Range(new Position(position.line, start), position)
-            }
-          })
-        result = new CompletionList(items)
-      }
-    }
-    return result
+    return new CompletionList([])
   }
 }
diff -r 8b67040b80ce -r fd26cf23e9b2 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Mon Jun 12 15:44:08 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Mon Jun 12 15:52:49 2017 +0200
@@ -123,14 +123,12 @@
 
 
     /* 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 */
 
diff -r 8b67040b80ce -r fd26cf23e9b2 src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Mon Jun 12 15:44:08 2017 +0200
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Mon Jun 12 15:52:49 2017 +0200
@@ -75,18 +75,6 @@
 }
 
 
-/* completion */
-
-export function complete_name(prefix: string): [string]
-{
-  let result = [] as [string]
-  for (const entry of names) {
-    if (entry[1].startsWith(prefix)) { result.push(entry[0]) }
-  }
-  return result.sort()
-}
-
-
 /* prettify symbols mode */
 
 interface PrettyStyleProperties