# HG changeset patch # User wenzelm # Date 1497275048 -7200 # Node ID 8b67040b80cedd7fe4a8fcf10937c86280343bc0 # Parent 65a68dcd95c3752427564a3d2df5faa787a2e017 tuned; diff -r 65a68dcd95c3 -r 8b67040b80ce src/Tools/VSCode/extension/src/symbol.ts --- a/src/Tools/VSCode/extension/src/symbol.ts Mon Jun 12 15:40:40 2017 +0200 +++ b/src/Tools/VSCode/extension/src/symbol.ts Mon Jun 12 15:44:08 2017 +0200 @@ -4,27 +4,26 @@ import { Disposable, DocumentSelector, ExtensionContext, extensions } from 'vscode'; -export type Symbol = string - - /* ASCII characters */ -export function is_char(s: string): boolean +export type Symbol = string + +export function is_char(s: Symbol): boolean { return s.length == 1 } -export function is_ascii_letter(s: string): boolean +export function is_ascii_letter(s: Symbol): boolean { return is_char(s) && "A" <= s && s <= "Z" || "a" <= s && s <= "z" } -export function is_ascii_digit(s: string): boolean +export function is_ascii_digit(s: Symbol): boolean { return is_char(s) && "0" <= s && s <= "9" } -export function is_ascii_quasi(s: string): boolean +export function is_ascii_quasi(s: Symbol): boolean { return s == "_" || s == "'" } -export function is_ascii_letdig(s: string): boolean +export function is_ascii_letdig(s: Symbol): boolean { return is_ascii_letter(s) || is_ascii_digit(s) || is_ascii_quasi(s) } -export function is_ascii_identifier(s: String): boolean +export function is_ascii_identifier(s: Symbol): boolean { const n = s.length