# HG changeset patch # User wenzelm # Date 1646841152 -3600 # Node ID 1b1b60db9ddaf7e78e7f436a9d05c395808f5953 # Parent 41dfe941c3da6833ec21ac8742e0fccb2a4f60ad clarified modules: vscode vs. extension; clarified signature; diff -r 41dfe941c3da -r 1b1b60db9dda src/Tools/VSCode/extension/src/isabelle_encoding.ts --- 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 = - new Map(static_symbols.map((s: Symbol_Entry) => [s.symbol, String.fromCharCode(s.code)])); - -export const symbols_encode: Map = - 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(); - } - }; -} diff -r 41dfe941c3da -r 1b1b60db9dda src/Tools/VSCode/extension/src/symbol.ts --- 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 { 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 = + new Map(static_symbols.map((s: Symbol_Code) => [s.symbol, String.fromCharCode(s.code)])); + +export const symbols_encode: Map = + 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(); + } + }; +} diff -r 41dfe941c3da -r 1b1b60db9dda src/Tools/VSCode/src/build_vscodium.scala --- 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)