# HG changeset patch # User wenzelm # Date 1646909798 -3600 # Node ID d1e5f9dbf88594adf28e37752a8c63ceec1b151c # Parent 5055c0cdabc96f6fafbb17835ffe25b6c66a155e clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode; diff -r 5055c0cdabc9 -r d1e5f9dbf885 lib/Tools/vscode --- a/lib/Tools/vscode Wed Mar 09 23:05:07 2022 +0100 +++ b/lib/Tools/vscode Thu Mar 10 11:56:38 2022 +0100 @@ -2,10 +2,11 @@ # # Author: Makarius # -# DESCRIPTION: run Isabelle/VSCode using local VSCodium installation +# DESCRIPTION: run Isabelle/VSCode (requires "vscodium-X.YY.Z" component) -DIR="$(isabelle vscode_setup -C)" || exit "$?" -exec "$DIR/bin/codium" \ +isabelle vscode_setup || exit "$?" + +exec "$ISABELLE_VSCODIUM_HOME/bin/codium" \ --locale en-US \ --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \ --extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \ diff -r 5055c0cdabc9 -r d1e5f9dbf885 src/Tools/VSCode/src/vscode_setup.scala --- a/src/Tools/VSCode/src/vscode_setup.scala Wed Mar 09 23:05:07 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_setup.scala Thu Mar 10 11:56:38 2022 +0100 @@ -1,7 +1,7 @@ /* Title: Tools/VSCode/src/vscode_setup.scala Author: Makarius -Setup VSCode from VSCodium distribution. +Provide user configuration for Isabelle/VSCode. */ package isabelle.vscode @@ -9,68 +9,13 @@ import isabelle._ -import java.security.MessageDigest -import java.util.Base64 - object VSCode_Setup { - /* global resources */ - - def vscode_home: Path = Path.variable("ISABELLE_VSCODE_HOME") - def vscode_settings: Path = Path.variable("ISABELLE_VSCODE_SETTINGS") - def vscode_settings_user: Path = vscode_settings + Path.explode("user-data/User/settings.json") - def version: String = Build_VSCodium.version - - def vscodium_home: Path = Path.variable("ISABELLE_VSCODIUM_HOME") - def vscodium_home_ok(): Boolean = - try { vscodium_home.is_dir } - catch { case ERROR(_) => false } - - def vscode_installation(info: Build_VSCodium.Platform_Info): (Boolean, Path) = - { - val install_dir = - info.platform_dir(vscode_settings + Path.basic("installation") + Path.basic(version)) - val install_ok = Build_VSCodium.vscodium_exe(install_dir).is_file - (install_ok, install_dir) - } - - - /* 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_lines(dir + Path.explode("app/product.json")) { _.map(line => - if (line.containsSlice(file_name) && line.contains(checksum1)) { - line.replace(checksum1, checksum2) - } - else line) - } - } - - /* vscode setup */ - def default_platform: Platform.Family.Value = Platform.family + def vscode_settings_user: Path = + Path.explode("$ISABELLE_VSCODE_SETTINGS/user-data/User/settings.json") private val init_settings = """ { "editor.fontFamily": "'Isabelle DejaVu Sans Mono'", @@ -86,87 +31,36 @@ } """ - def vscode_setup( - check: Boolean = false, - platform: Platform.Family.Value = default_platform, - quiet: Boolean = false, - fresh: Boolean = false, - progress: Progress = new Progress): Unit = + def vscode_setup(): Unit = { - val platform_info = Build_VSCodium.the_platform_info(platform) - val (install_ok, install_dir) = vscode_installation(platform_info) + if (Isabelle_System.getenv("ISABELLE_VSCODIUM_HOME").isEmpty) { + error("""Missing $ISABELLE_VSCODIUM_HOME: proper vscodium-X.YY.Z component required""") + } if (!vscode_settings_user.is_file) { Isabelle_System.make_directory(vscode_settings_user.dir) File.write(vscode_settings_user, init_settings) } - - if (check) { - if (vscodium_home_ok()) { - progress.echo(vscodium_home.expand.implode) - } - else if (install_ok) { - progress.echo(install_dir.expand.implode) - } - else { - error("Bad Isabelle/VSCode installation: " + install_dir.expand + - "\n(use \"isabelle vscode_setup\" for download and installation)") - } - } - else { - if (install_ok) { - progress.echo_warning("Isabelle/VSCode installation already present: " + install_dir.expand) - } - if (!install_ok || fresh) { - Isabelle_System.make_directory(install_dir) - platform_info.download(install_dir, progress = if (quiet) new Progress else progress) - platform_info.patch_resources(install_dir) - platform_info.setup_executables(install_dir) - } - } } /* Isabelle tool wrapper */ val isabelle_tool = - Isabelle_Tool("vscode_setup", "setup VSCode from VSCodium distribution", + Isabelle_Tool("vscode_setup", "provide user configuration for Isabelle/VSCode", Scala_Project.here, args => { - var check = false - var fresh = false - var platforms = List(default_platform) - var quiet = false - val getopts = Getopts(""" -Usage: vscode_setup [OPTIONS] +Usage: vscode_setup - Options are: - -C check and print installation directory - -f force fresh installation - -p NAMES platform families: comma-separated names - (""" + commas_quote(Platform.Family.list.map(_.toString)) + """, default: """ + - quote(default_platform.toString) + """) - -q quiet mode - - Maintain local installation of VSCode, see also https://vscodium.com - - Option -C checks the existing installation (without download), and - prints its directory location. + Provide user configuration for Isabelle/VSCode. The following initial settings are provided for a fresh installation: -""" + init_settings, - "C" -> (_ => check = true), - "f" -> (_ => fresh = true), - "p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)), - "q" -> (_ => quiet = true)) +""" + init_settings) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() - val progress = new Console_Progress() - for (platform <- platforms) { - vscode_setup(check = check, platform = platform, quiet = quiet, fresh = fresh, progress = progress) - } + vscode_setup() }) }