--- a/src/Tools/VSCode/extension/MANIFEST Wed Jul 17 21:02:30 2024 +0200
+++ b/src/Tools/VSCode/extension/MANIFEST Wed Jul 17 21:03:56 2024 +0200
@@ -13,8 +13,6 @@
media/vscode.css
package.json
README.md
-src/abbreviations.ts
-src/completion.ts
src/decorations.ts
src/extension.ts
src/file.ts
@@ -22,11 +20,9 @@
src/lsp.ts
src/output_view.ts
src/platform.ts
-src/prefix_tree.ts
src/preview_panel.ts
src/script_decorations.ts
src/state_panel.ts
-src/symbol.ts
src/vscode_lib.ts
test/extension.test.ts
test/index.ts
--- a/src/Tools/VSCode/extension/src/abbreviations.ts Wed Jul 17 21:02:30 2024 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,148 +0,0 @@
-/* Author: Denis Paluca, TU Muenchen
-
-Input abbreviation and autocompletion of Isabelle symbols.
-*/
-
-'use strict';
-
-import { ExtensionContext, Range, TextDocumentContentChangeEvent, workspace, WorkspaceEdit } from 'vscode'
-import { Prefix_Tree } from './prefix_tree'
-import * as library from './library'
-import * as vscode_lib from './vscode_lib'
-import * as symbol from './symbol'
-
-const entries: Record<string, string> = {}
-const prefix_tree: Prefix_Tree = new Prefix_Tree()
-
-function register_abbreviations(data: symbol.Entry[], context: ExtensionContext)
-{
- const [min_length, max_length] = set_abbrevs(data)
- const alphanumeric_regex = /[^A-Za-z0-9 ]/
- context.subscriptions.push(
- workspace.onDidChangeTextDocument(e =>
- {
- const doc = e.document
- const mode = vscode_lib.get_replacement_mode()
- if (
- mode === 'none' ||
- doc.languageId !== 'isabelle' ||
- doc.uri.scheme !== 'isabelle'
- ) { return; }
- const edits = new WorkspaceEdit()
-
- const changes = e.contentChanges.slice(0)
- changes.sort((c1, c2) => c1.rangeOffset - c2.rangeOffset)
-
- let c: TextDocumentContentChangeEvent
- while (c = changes.pop()) {
- if (c.rangeLength === 1 || library.has_newline(c.text)) {
- return
- }
-
- const end_offset = c.rangeOffset + c.text.length +
- changes.reduce((a,b) => a + b.text.length, 0)
-
- if (end_offset < min_length) {
- continue
- }
-
- const start_offset = end_offset < max_length ? 0 : end_offset - max_length
-
- const end_pos = doc.positionAt(end_offset)
- let start_pos = doc.positionAt(start_offset)
- let range = new Range(start_pos, end_pos)
- const text = library.reverse(doc.getText(range))
-
- const node = prefix_tree.get_end_or_value(text)
- if (!node || !node.value) {
- continue
- }
-
- const word = node.get_word().join('')
- if (mode === 'non-alphanumeric' && !alphanumeric_regex.test(word)) {
- continue
- }
-
- start_pos = doc.positionAt(end_offset - word.length)
- range = new Range(start_pos, end_pos)
-
- edits.replace(doc.uri, range, node.value as string)
- }
-
- apply_edits(edits)
- })
- )
-}
-
-async function apply_edits(edit: WorkspaceEdit)
-{
- await waitForNextTick()
- await workspace.applyEdit(edit)
-}
-
-function waitForNextTick(): Promise<void> {
- return new Promise((res) => setTimeout(res, 0));
-}
-
-function get_unique_abbrevs(data: symbol.Entry[]): Set<string>
-{
- const unique = new Set<string>()
- const non_unique = new Set<string>()
- for (const {code, abbrevs} of data) {
- for (const abbrev of abbrevs) {
- if (abbrev.length === 1 || non_unique.has(abbrev)) {
- continue
- }
-
- if (unique.has(abbrev)) {
- non_unique.add(abbrev)
- unique.delete(abbrev)
- entries[abbrev] = undefined
- continue
- }
-
-
- entries[abbrev] = String.fromCharCode(code)
- unique.add(abbrev)
- }
- }
- return unique
-}
-
-function set_abbrevs(data: symbol.Entry[]): [number, number]
-{
- const unique = get_unique_abbrevs(data)
-
- // Add white space to abbrevs which are prefix of other abbrevs
- for (const a1 of unique) {
- for (const a2 of unique) {
- if (a1 === a2) {
- continue
- }
-
- if (a2.startsWith(a1)) {
- const val = entries[a1]
- delete entries[a1]
- entries[a1 + ' '] = val
- break
- }
- }
- }
-
- let min_length: number
- let max_length: number
- for (const entry in entries) {
- if (!min_length || min_length > entry.length)
- min_length = entry.length
-
- if (!max_length || max_length< entry.length)
- max_length = entry.length
-
- // add reverse because we check the abbrevs from the end
- prefix_tree.insert(library.reverse(entry), entries[entry])
- }
-
- return [min_length, max_length]
-}
-
-export { register_abbreviations }
--- a/src/Tools/VSCode/extension/src/completion.ts Wed Jul 17 21:02:30 2024 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-/* Author: Makarius
-
-Support for PIDE completion information.
-*/
-
-'use strict';
-
-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
-
- return new CompletionList([])
- }
-}
--- a/src/Tools/VSCode/extension/src/prefix_tree.ts Wed Jul 17 21:02:30 2024 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-/* Author: Denis Paluca, TU Muenchen
-
-Prefix tree for symbol autocompletion.
-*/
-
-'use strict';
-
-class Tree_Node
-{
- public key: number | string
- public parent: Tree_Node = null
- public end: boolean = false
- public value: number[] | string
- public children: Record<number | string, Tree_Node> = {}
- constructor(key: number | string)
- {
- this.key = key
- }
-
- public get_word(): number[] | string[]
- {
- let output = []
- let node: Tree_Node = this
-
- while (node.key !== null) {
- output.unshift(node.key)
- node = node.parent
- }
-
- return output
- }
-}
-
-class Prefix_Tree
-{
- private root: Tree_Node
-
- constructor()
- {
- this.root = new Tree_Node(null)
- }
-
- public insert(word: number[] | string, value: number[] | string)
- {
- let node = this.root
- for (var i = 0; i < word.length; i++) {
- if (!node.children[word[i]]) {
- node.children[word[i]] = new Tree_Node(word[i])
-
- node.children[word[i]].parent = node
- }
-
- node = node.children[word[i]]
- node.end = false
-
- if (i === word.length-1) {
- node.end = true
- node.value = value
- }
- }
- }
-
- public get_node(prefix: number[] | string): Tree_Node | undefined
- {
- let node = this.root
-
- for (let i = 0; i < prefix.length; i++) {
- if (!node.children[prefix[i]]) {
- return
- }
- node = node.children[prefix[i]]
- }
- return node
- }
-
- public get_end_or_value(prefix: number[] | string): Tree_Node | undefined
- {
- let node = this.root
- let resNode: Tree_Node
- for (let i = 0; i < prefix.length; i++) {
- if (!node.children[prefix[i]]) {
- return resNode
- }
- node = node.children[prefix[i]]
- if (node.value) {
- resNode = node
- }
-
- if (node.end) {
- return node
- }
- }
- return node
- }
-}
-
-export { Prefix_Tree, Tree_Node }
--- a/src/Tools/VSCode/extension/src/symbol.ts Wed Jul 17 21:02:30 2024 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-/* Author: Makarius
-
-Isabelle text symbols versus UTF-8/Unicode encoding. See also:
-
- - Pure/General/symbol.scala
- - Pure/General/utf8.scala
- - https://encoding.spec.whatwg.org
-*/
-
-'use strict';
-
-import * as file from './file'
-import * as library from './library'
-
-
-/* ASCII characters */
-
-export type Symbol = string
-
-export function is_char(s: Symbol): boolean
-{ return s.length === 1 }
-
-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: Symbol): boolean
-{ return is_char(s) && "0" <= s && s <= "9" }
-
-export function is_ascii_quasi(s: Symbol): boolean
-{ return s === "_" || s === "'" }
-
-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: Symbol): 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
-}
-
-
-/* defined symbols */
-
-export interface Entry {
- symbol: string;
- name: string;
- abbrevs: string[];
- code?: number;
-}
-
-export class Symbols
-{
- entries: Entry[]
- private entries_map: Map<Symbol, Entry>
-
- constructor(entries: Entry[])
- {
- this.entries = entries
- this.entries_map = new Map<Symbol, Entry>()
- for (const entry of entries) {
- this.entries_map.set(entry.symbol, entry)
- }
- }
-
- public get(sym: Symbol): Entry | undefined
- {
- return this.entries_map.get(sym)
- }
-
- public defined(sym: Symbol): boolean
- {
- return this.entries_map.has(sym)
- }
-}
-
-function load_symbols(): Entry[]
-{
- const vscodium_resources = library.getenv("ISABELLE_VSCODIUM_RESOURCES")
- if (vscodium_resources) {
- const path = vscodium_resources + "/vscodium/out/vs/base/browser/ui/fonts/symbols.json"
- return file.read_json_sync(file.platform_path(path))
- }
- else { return [] }
-}
-
-export const symbols: Symbols = new Symbols(load_symbols())