diff -r 41dfe941c3da -r 1b1b60db9dda src/Tools/VSCode/patches/isabelle_encoding.ts
--- /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();
+    }
+  };
+}