# HG changeset patch
# User wenzelm
# Date 1646684172 -3600
# Node ID 83197a0ac6df75cabb1c8d45090db5adad802663
# Parent  ef9f9d43b867a57a2b1322ddd4f40718aefd5d14
towards UTF-8-Isabelle symbol encoding;

diff -r ef9f9d43b867 -r 83197a0ac6df lib/Tools/vscode
--- a/lib/Tools/vscode	Mon Mar 07 17:18:19 2022 +0100
+++ b/lib/Tools/vscode	Mon Mar 07 21:16:12 2022 +0100
@@ -4,6 +4,8 @@
 #
 # DESCRIPTION: run Isabelle/VSCode using local VSCodium installation
 
+export ISABELLE_VSCODE_SYMBOLS="$(platform_path "$ISABELLE_VSCODE_WORKSPACE/symbols.json")"
+
 DIR="$(isabelle vscode_setup -C)" || exit "$?"
 exec "$DIR/bin/codium" \
   --locale en-US \
diff -r ef9f9d43b867 -r 83197a0ac6df src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Mon Mar 07 17:18:19 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Mon Mar 07 21:16:12 2022 +0100
@@ -33,8 +33,7 @@
   try {
     const isabelle_home = library.getenv_strict("ISABELLE_HOME")
 
-    const symbols = await symbol.load_symbols(library.workspace_path("symbols.json"))
-    const workspace_dir = await Isabelle_Workspace.register(context, symbols)
+    const workspace_dir = await Isabelle_Workspace.register(context, symbol.symbols)
     const roots = workspace.workspaceFile === undefined ? await workspace.findFiles("{ROOT,ROOTS}") : []
 
     const isabelle_tool = isabelle_home + "/bin/isabelle"
diff -r ef9f9d43b867 -r 83197a0ac6df src/Tools/VSCode/extension/src/isabelle_encoding.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/isabelle_encoding.ts	Mon Mar 07 21:16:12 2022 +0100
@@ -0,0 +1,64 @@
+/*  Author:     Makarius
+
+UTF-8-Isabelle symbol encoding: minimal dependencies, for use inside VSCode.
+*/
+
+'use strict';
+
+import * as fs from 'fs'
+import { TextEncoder, TextDecoder } from 'util'
+
+
+/* defined symbols */
+
+export interface Symbol_Entry
+{
+  symbol: string,
+  name: string,
+  code: number,
+  abbrevs: string[]
+}
+
+const symbols_file = process.env["ISABELLE_VSCODE_SYMBOLS"]
+
+export const symbols: [Symbol_Entry] =
+  symbols_file ? JSON.parse(fs.readFileSync(symbols_file).toString()) : []
+
+export const symbols_decode: Map<string, string> =
+  new Map(symbols.map((s: Symbol_Entry) => [s.symbol, String.fromCharCode(s.code)]))
+
+export const symbols_encode: Map<string, string> =
+  new Map(symbols.map((s: Symbol_Entry) => [String.fromCharCode(s.code), s.symbol]))
+
+
+/* encoding */
+
+export const UTF8_Isabelle = 'utf8-isabelle'
+
+export interface Options {
+  stripBOM?: boolean;
+  addBOM?: boolean;
+  defaultEncoding?: string;
+}
+
+export interface EncoderStream {
+  write(str: string): Uint8Array
+  end(): Uint8Array | undefined
+}
+
+export interface DecoderStream {
+  write(buf: Uint8Array): string
+  end(): string | undefined
+}
+
+export function getEncoder(encoding: string, options?: Options): EncoderStream
+{
+  const utf8_encoder = new TextEncoder
+  return null
+}
+
+export function getDecoder(encoding: string, options?: Options): DecoderStream
+{
+  const utf8_decoder = new TextDecoder
+  return null
+}
diff -r ef9f9d43b867 -r 83197a0ac6df src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Mon Mar 07 17:18:19 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Mon Mar 07 21:16:12 2022 +0100
@@ -10,6 +10,7 @@
 'use strict';
 
 import * as file from './file'
+import * as isabelle_encoding from './isabelle_encoding'
 
 
 /* ASCII characters */
@@ -44,13 +45,7 @@
 
 /* defined symbols */
 
-export interface Entry
-{
-  symbol: Symbol,
-  name: string,
-  code: number,
-  abbrevs: string[]
-}
+export type Entry = isabelle_encoding.Symbol_Entry
 
 export class Symbols
 {
@@ -75,17 +70,6 @@
   {
     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 async function load_symbols(path: string): Promise<Symbols>
-{
-  const entries = await file.read_json<[Entry]>(path)
-  return new Symbols(entries)
-}
+export const symbols: Symbols = new Symbols(isabelle_encoding.symbols)