# HG changeset patch # User wenzelm # Date 1645908053 -3600 # Node ID 0b6c43a87fa6e17779c28df4d7df234c734547e4 # Parent 3b5aa38282bd72e417699c3e416acdf2e5e8be23 support Isabelle fonts via patch of vscode resources; diff -r 3b5aa38282bd -r 0b6c43a87fa6 src/Tools/VSCode/src/vscode_setup.scala --- a/src/Tools/VSCode/src/vscode_setup.scala Fri Feb 25 16:54:50 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_setup.scala Sat Feb 26 21:40:53 2022 +0100 @@ -9,6 +9,9 @@ import isabelle._ +import java.security.MessageDigest +import java.util.Base64 + object VSCode_Setup { @@ -33,6 +36,39 @@ } + /* patch resources */ + + // see https://github.com/microsoft/vscode/blob/main/build/gulpfile.vscode.js + // function computeChecksum(filename) + + def file_checksum(path: Path): String = + { + val digest = MessageDigest.getInstance("MD5") + digest.update(Bytes.read(path).array) + Bytes(Base64.getEncoder.encode(digest.digest())) + .text.replaceAll("=", "") + } + + def patch_resources(dir: Path): Unit = + { + HTML.init_fonts(dir + Path.explode("app/out/vs/base/browser/ui")) + + val workbench_css = dir + Path.explode("app/out/vs/workbench/workbench.desktop.main.css") + val checksum1 = file_checksum(workbench_css) + File.append(workbench_css, "\n\n" + HTML.fonts_css_dir(prefix = "../base/browser/ui")) + val checksum2 = file_checksum(workbench_css) + + val file_name = workbench_css.file_name + File.change(dir + Path.explode("app/product.json"), text => + cat_lines(split_lines(text).map(line => + if (line.containsSlice(file_name) && line.contains(checksum1)) { + line.replace(checksum1, checksum2) + } + else line + ))) + } + + /* vscode setup */ val default_download_url: String = "https://github.com/VSCodium/vscodium/releases/download" @@ -106,6 +142,7 @@ Isabelle_System.gnutar("-xzf " + File.bash_path(download), dir = install_dir).check } + platform match { case Platform.Family.macos => Isabelle_System.make_directory(exe.dir) @@ -119,6 +156,12 @@ for (file <- files1 ::: files2) File.set_executable(File.path(file), true) case _ => } + + patch_resources( + if (platform == Platform.Family.macos) { + install_dir + Path.explode("VSCodium.app/Contents/Resources") + } + else install_dir + Path.explode("resources")) }) } }