# HG changeset patch
# User wenzelm
# Date 1497123245 -7200
# Node ID b2bfbefd354f749c12fe7a21f473ec9bc13b28f9
# Parent  5a6b67e42c4aa162f72df118f4accfa33a1bc0cf
symbol completion that bypasses the LS protocol, and thus observes the range properly;
more symbol operations;

diff -r 5a6b67e42c4a -r b2bfbefd354f src/Tools/VSCode/extension/src/completion.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/completion.ts	Sat Jun 10 21:34:05 2017 +0200
@@ -0,0 +1,36 @@
+'use strict';
+
+import * as symbol from './symbol'
+import { CompletionItemProvider, CompletionItem, TextDocument, Range, Position,
+  CancellationToken, CompletionList } from 'vscode'
+
+export class Completion_Provider implements CompletionItemProvider
+{
+  public provideCompletionItems(
+    document: TextDocument, position: Position, token: CancellationToken): CompletionList
+  {
+    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
+  }
+}
diff -r 5a6b67e42c4a -r b2bfbefd354f src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Sat Jun 10 14:54:56 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sat Jun 10 21:34:05 2017 +0200
@@ -7,7 +7,8 @@
 import * as preview from './preview';
 import * as protocol from './protocol';
 import * as symbol from './symbol';
-import { ExtensionContext, workspace, window, commands } from 'vscode';
+import * as completion from './completion';
+import { ExtensionContext, workspace, window, commands, languages } from 'vscode';
 import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
   from 'vscode-languageclient';
 
@@ -121,6 +122,15 @@
     })
 
 
+    /* completion */
+
+    const completion_provider = new completion.Completion_Provider
+    for (const mode of ["isabelle", "isabelle-ml"]) {
+      context.subscriptions.push(
+        languages.registerCompletionItemProvider(mode, completion_provider))
+    }
+
+
     /* start server */
 
     context.subscriptions.push(language_client.start())
diff -r 5a6b67e42c4a -r b2bfbefd354f src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Sat Jun 10 14:54:56 2017 +0200
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Sat Jun 10 21:34:05 2017 +0200
@@ -2,6 +2,37 @@
 
 export type Symbol = string
 
+
+/* ASCII characters */
+
+export function is_char(s: string): boolean
+{ return s.length == 1 }
+
+export function is_ascii_letter(s: string): boolean
+{ return is_char(s) && "A" <= s && s <= "Z" || "a" <= s && s <= "z" }
+
+export function is_ascii_digit(s: string): boolean
+{ return is_char(s) && "0" <= s && s <= "9" }
+
+export function is_ascii_quasi(s: string): boolean
+{ return s == "_" || s == "'" }
+
+export function is_ascii_letdig(s: string): boolean
+{ return is_ascii_letter(s) || is_ascii_digit(s) || is_ascii_quasi(s) }
+
+export function is_ascii_identifier(s: String): boolean
+{
+  const n = s.length
+
+  let all_letdig = true
+  for (const c of s) { all_letdig = all_letdig && is_ascii_letdig(c) }
+
+  return n > 0 && is_ascii_letter(s.charAt(0)) && all_letdig
+}
+
+
+/* named symbols */
+
 export interface Entry
 {
   symbol: Symbol,
@@ -38,4 +69,16 @@
     names.set(entry.symbol, entry.name)
     codes.set(entry.symbol, entry.code)
   }
+}
+
+
+/* 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()
 }
\ No newline at end of file