# 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