# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1721243036 -7200
# Node ID ca20bd1e25fe48e6cb1f66ce75c042c9f9b3287e
# Parent  664c1a6cc8c1b2991dc1d8b99e0dc635e2947fad
vscode: removed unused code;

diff -r 664c1a6cc8c1 -r ca20bd1e25fe src/Tools/VSCode/extension/MANIFEST
--- 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
diff -r 664c1a6cc8c1 -r ca20bd1e25fe src/Tools/VSCode/extension/src/abbreviations.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 }
diff -r 664c1a6cc8c1 -r ca20bd1e25fe src/Tools/VSCode/extension/src/completion.ts
--- 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([])
-  }
-}
diff -r 664c1a6cc8c1 -r ca20bd1e25fe src/Tools/VSCode/extension/src/prefix_tree.ts
--- 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 }
diff -r 664c1a6cc8c1 -r ca20bd1e25fe src/Tools/VSCode/extension/src/symbol.ts
--- 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())