clarified modules: vscode vs. extension;
clarified signature;

--- a/src/Tools/VSCode/extension/src/isabelle_encoding.ts	Wed Mar 09 16:21:14 2022 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-/*  Author:     Makarius
-
-UTF-8-Isabelle symbol encoding: for use inside VSCode.
-*/
-
-'use strict';
-
-import { TextEncoder, TextDecoder } from 'util'   // VSCODE: REMOVE
-
-
-/* defined symbols */
-
-export interface Symbol_Entry {
-  symbol: string;
-  name: string;
-  code: number;
-  abbrevs: string[];
-}
-
-export const static_symbols: Symbol_Entry[] = [/*symbols*/];
-
-export const symbols_decode: Map<string, string> =
-  new Map(static_symbols.map((s: Symbol_Entry) => [s.symbol, String.fromCharCode(s.code)]));
-
-export const symbols_encode: Map<string, string> =
-  new Map(static_symbols.map((s: Symbol_Entry) => [String.fromCharCode(s.code), s.symbol]));
-
-
-/* encoding */
-
-export const ENCODING = 'utf8isabelle';
-export const LABEL = 'UTF-8-Isabelle';
-
-export interface Options {
-  stripBOM?: boolean;
-  addBOM?: boolean;
-  defaultEncoding?: string;
-}
-
-export interface IEncoderStream {
-  write(input: string): Uint8Array;
-  end(): Uint8Array | undefined;
-}
-
-export interface IDecoderStream {
-  write(input: Uint8Array): string;
-  end(): string | undefined;
-}
-
-export function getEncoder(): IEncoderStream {
-  const utf8_encoder = new TextEncoder();
-  return {
-    write(input: string): Uint8Array {
-      return utf8_encoder.encode(input);
-    },
-    end(): Uint8Array | undefined {
-      return utf8_encoder.encode();
-    }
-  };
-}
-
-export function getDecoder(): IDecoderStream {
-  const utf8TextDecoder = new TextDecoder();
-  return {
-    write(input: Uint8Array): string {
-      return utf8TextDecoder.decode(input, { stream: true });
-    },
-    end(): string | undefined {
-      return utf8TextDecoder.decode();
-    }
-  };
-}

--- a/src/Tools/VSCode/extension/src/symbol.ts	Wed Mar 09 16:21:14 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Wed Mar 09 16:52:32 2022 +0100
@@ -11,7 +11,6 @@
 
 import * as file from './file'
 import * as library from './library'
-import * as isabelle_encoding from './isabelle_encoding'
 
 
 /* ASCII characters */
@@ -46,7 +45,12 @@
 
 /* defined symbols */
 
-export type Entry = isabelle_encoding.Symbol_Entry
+export interface Entry {
+  symbol: string;
+  name: string;
+  abbrevs: string[];
+  code?: number;
+}
 
 export class Symbols
 {

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/patches/isabelle_encoding.ts	Wed Mar 09 16:52:32 2022 +0100
@@ -0,0 +1,68 @@
+/*  Author:     Makarius
+
+UTF-8-Isabelle symbol encoding: for use inside VSCode.
+*/
+
+'use strict';
+
+
+/* defined symbols */
+
+export interface Symbol_Code {
+  symbol: string;
+  code: number;
+}
+
+export const static_symbols: Symbol_Code[] = [/*symbols*/];
+
+export const symbols_decode: Map<string, string> =
+  new Map(static_symbols.map((s: Symbol_Code) => [s.symbol, String.fromCharCode(s.code)]));
+
+export const symbols_encode: Map<string, string> =
+  new Map(static_symbols.map((s: Symbol_Code) => [String.fromCharCode(s.code), s.symbol]));
+
+
+/* encoding */
+
+export const ENCODING = 'utf8isabelle';
+export const LABEL = 'UTF-8-Isabelle';
+
+export interface Options {
+  stripBOM?: boolean;
+  addBOM?: boolean;
+  defaultEncoding?: string;
+}
+
+export interface IEncoderStream {
+  write(input: string): Uint8Array;
+  end(): Uint8Array | undefined;
+}
+
+export interface IDecoderStream {
+  write(input: Uint8Array): string;
+  end(): string | undefined;
+}
+
+export function getEncoder(): IEncoderStream {
+  const utf8_encoder = new TextEncoder();
+  return {
+    write(input: string): Uint8Array {
+      return utf8_encoder.encode(input);
+    },
+    end(): Uint8Array | undefined {
+      return utf8_encoder.encode();
+    }
+  };
+}
+
+export function getDecoder(): IDecoderStream {
+  const utf8TextDecoder = new TextDecoder();
+  return {
+    write(input: Uint8Array): string {
+      return utf8TextDecoder.decode(input, { stream: true });
+    },
+    end(): string | undefined {
+      return utf8TextDecoder.decode();
+    }
+  };
+}

--- a/src/Tools/VSCode/src/build_vscodium.scala	Wed Mar 09 16:21:14 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Wed Mar 09 16:52:32 2022 +0100
@@ -26,22 +26,36 @@
   def vscodium_exe(dir: Path): Path = dir + Path.explode("bin/codium")
 
 
-  /* Isabelle symbols (static subset) */
-
-  val symbols_json: Path = Path.explode("symbols.json")
+  /* Isabelle symbols (static subset only) */
 
-  def write_symbols(dir: Path, json: List[JSON.T]): Unit =
-    File.write(Isabelle_System.make_directory(dir) + symbols_json, JSON.Format.apply_lines(json))
-
-  def load_symbols_static(): List[JSON.T] =
+  def make_symbols(): File.Content =
   {
     val symbols = Symbol.Symbols.load(static = true)
-    for (entry <- symbols.entries; code <- entry.code)
-      yield JSON.Object(
-        "symbol" -> entry.symbol,
-        "name" -> entry.name,
-        "code" -> code,
-        "abbrevs" -> entry.abbrevs)
+    val symbols_js =
+      JSON.Format.apply_lines(
+        for (entry <- symbols.entries) yield
+          JSON.Object(
+            "symbol" -> entry.symbol,
+            "name" -> entry.name,
+            "abbrevs" -> entry.abbrevs) ++
+          JSON.optional("code", entry.code))
+
+    File.Content(Path.explode("symbols.json"), symbols_js)
+  }
+
+  def make_isabelle_encoding(header: String): File.Content =
+  {
+    val symbols = Symbol.Symbols.load(static = true)
+    val symbols_js =
+      JSON.Format.apply_lines(
+        for (entry <- symbols.entries; code <- entry.code)
+          yield JSON.Object("symbol" -> entry.symbol, "code" -> code))
+
+    val path = Path.explode("isabelle_encoding.ts")
+    val body =
+      File.read(Path.explode("$ISABELLE_VSCODE_HOME/patches") + path)
+        .replace("[/*symbols*/]", symbols_js)
+    File.Content(path, header + "\n" + body)
   }
 
 
@@ -119,22 +133,11 @@
 
         // isabelle_encoding.ts
         {
-          val isabelle_encodings =
-            Path.explode("$ISABELLE_VSCODE_HOME/extension/src/isabelle_encoding.ts")
           val common_dir = dir + Path.explode("src/vs/workbench/services/textfile/common")
-
-          val inline_symbols = JSON.Format.apply_lines(load_symbols_static())
-
           val header =
             split_lines(File.read(common_dir + Path.explode("encoding.ts")))
               .takeWhile(_.trim.nonEmpty)
-          val body =
-            for {
-              line <- split_lines(File.read(isabelle_encodings))
-              if !line.containsSlice("// VSCODE: REMOVE")
-            } yield line.replace("[/*symbols*/]", inline_symbols)
-
-          File.write(common_dir + isabelle_encodings.base, cat_lines(header ::: body))
+          make_isabelle_encoding(cat_lines(header)).write(common_dir)
         }
 
         // explicit patches
@@ -159,7 +162,7 @@
       Isabelle_System.with_copy_dir(dir, dir.orig) {
         val fonts_dir = dir + Path.explode("app/out/vs/base/browser/ui/fonts")
         HTML.init_fonts(fonts_dir.dir)
-        write_symbols(fonts_dir, load_symbols_static())
+        make_symbols().write(fonts_dir)
 
         val workbench_css = dir + Path.explode("app/out/vs/workbench/workbench.desktop.main.css")
         val checksum1 = file_checksum(workbench_css)