src/Tools/VSCode/extension/src/symbol.ts
changeset 75209 4187f6f18232
parent 75180 75695a504822
child 75210 d2add317268f
--- a/src/Tools/VSCode/extension/src/symbol.ts	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Thu Mar 03 20:04:27 2022 +0100
@@ -6,7 +6,7 @@
 'use strict';
 
 import * as library from './library'
-import { Disposable, DocumentSelector, ExtensionContext, extensions, window } from 'vscode'
+import * as file from './file'
 
 
 /* ASCII characters */
@@ -39,7 +39,7 @@
 }
 
 
-/* named symbols */
+/* defined symbols */
 
 export interface Entry
 {
@@ -49,33 +49,40 @@
   abbrevs: string[]
 }
 
-let symbol_entries: [Entry]
-const names = new Map<Symbol, string>()
-const codes = new Map<Symbol, number>()
-
-export function get_name(sym: Symbol): string | undefined
+export class Symbols
 {
-  return names.get(sym)
-}
+  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)
+    }
+  }
 
-export function get_code(sym: Symbol): number | undefined
-{
-  return codes.get(sym)
+  public get(sym: Symbol): Entry | undefined
+  {
+    return this.entries_map.get(sym)
+  }
+
+  public defined(sym: Symbol): boolean
+  {
+    return this.entries_map.has(sym)
+  }
+
+  public decode(sym: Symbol): string | undefined
+  {
+    const entry = this.get(sym)
+    const code = entry ? entry.code : undefined
+    return code ? String.fromCharCode(code) : undefined
+  }
 }
 
-export function get_unicode(sym: Symbol): string
-{
-  const code = get_code(sym)
-  return code ? String.fromCharCode(code) : ""
-}
-
-function update_entries(entries: [Entry])
+export async function load_symbols(path: string): Promise<Symbols>
 {
-  symbol_entries = entries
-  names.clear
-  codes.clear
-  for (const entry of entries) {
-    names.set(entry.symbol, entry.name)
-    codes.set(entry.symbol, entry.code)
-  }
+  const entries = await file.read_json<[Entry]>(file.platform_path(path))
+  return new Symbols(entries)
 }