# HG changeset patch # User wenzelm # Date 1648162480 -3600 # Node ID 4598cf29ef9880d5409b1c9600d144e3c36625fa # Parent c3f1bf2824bcd4cf494b795ed52fc09cae6d09d1# Parent 381082508063c18f4682431d303ece354cb57724 merged diff -r c3f1bf2824bc -r 4598cf29ef98 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Mar 24 22:43:41 2022 +0000 +++ b/Admin/components/components.sha1 Thu Mar 24 23:54:40 2022 +0100 @@ -446,6 +446,8 @@ c11d1120fcefaec79f099fe2be05b03cd2aed8b9 verit-2021.06-rmx.tar.gz b576fd5d89767c1067541d4839fb749c6a68d22c verit-2021.06.1-rmx.tar.gz 19c6e5677b0a26cbc5805da79d00d06a66b7a671 verit-2021.06.2-rmx.tar.gz +c4666a6d8080b5e376b50471fd2d9edeb1f9c988 vscode_extension-20220324.tar.gz +67b271186631f84efd97246bf85f6d8cfaa5edfd vscodium-1.65.2.tar.gz 81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz diff -r c3f1bf2824bc -r 4598cf29ef98 Admin/components/main --- a/Admin/components/main Thu Mar 24 22:43:41 2022 +0000 +++ b/Admin/components/main Thu Mar 24 23:54:40 2022 +0100 @@ -29,6 +29,8 @@ stack-2.7.3 vampire-4.6 verit-2021.06.2-rmx +vscode_extension-20220324 +vscodium-1.65.2 xz-java-1.9 z3-4.4.0_4.4.1 zipperposition-2.1-1 diff -r c3f1bf2824bc -r 4598cf29ef98 NEWS --- a/NEWS Thu Mar 24 22:43:41 2022 +0000 +++ b/NEWS Thu Mar 24 23:54:40 2022 +0100 @@ -15,9 +15,15 @@ *** Isabelle/VSCode Prover IDE *** -* Command-line tools "isabelle vscode_setup" and "isabelle vscode" -provide convenient access to a well-defined version of VSCodium -(open-source distribution of VSCode without MS telemetry). +* VSCodium, an open-source distribution of VSCode without MS +telemetry, has been bundled with Isabelle as add-on component. The +command-line tool "isabelle vscode" automatically configures it as +Isabelle/VSCode and starts the application. + +* Command-line tools "isabelle electron" and "isabelle node" provide +access to the underlying technologies of VSCodium, for use in other +applications. This essentially provides a freely programmable Chromium +browser engine that works uniformly on all platforms. *** HOL *** diff -r c3f1bf2824bc -r 4598cf29ef98 src/Tools/VSCode/src/build_vscode_extension.scala --- a/src/Tools/VSCode/src/build_vscode_extension.scala Thu Mar 24 22:43:41 2022 +0000 +++ b/src/Tools/VSCode/src/build_vscode_extension.scala Thu Mar 24 23:54:40 2022 +0100 @@ -1,7 +1,7 @@ /* Title: Tools/VSCode/src/build_vscode_extension.scala Author: Makarius -Build the Isabelle/VSCode extension. +Build the Isabelle/VSCode extension as component. */ package isabelle.vscode @@ -138,28 +138,63 @@ /* build extension */ def build_extension(options: Options, + target_dir: Path = Path.current, logic: String = default_logic, dirs: List[Path] = Nil, - progress: Progress = new Progress): File.Content = + progress: Progress = new Progress): Unit = { Isabelle_System.require_command("node") Isabelle_System.require_command("yarn") Isabelle_System.require_command("vsce") - Isabelle_System.with_tmp_dir("build")(build_dir => - { - VSCode_Main.extension_manifest().prepare_dir(build_dir) + + /* component */ + + val component_name = "vscode_extension-" + Date.Format.alt_date(Date.now()) + val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name)) + progress.echo("Component " + component_dir) + + + /* build */ - build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress) + val vsix_name = + Isabelle_System.with_tmp_dir("build")(build_dir => + { + VSCode_Main.extension_manifest().prepare_dir(build_dir) + + build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress) + + val result = + progress.bash("yarn && vsce package", cwd = build_dir.file, echo = true).check + val Pattern = """.*Packaged:.*(isabelle-.*\.vsix).*""".r + val vsix_name = + result.out_lines.collectFirst({ case Pattern(name) => name }) + .getOrElse(error("Failed to guess resulting .vsix file name")) - val result = - progress.bash("yarn && vsce package", cwd = build_dir.file, echo = true).check - val Pattern = """.*Packaged:.*(isabelle-.*\.vsix).*""".r - val path = - result.out_lines.collectFirst({ case Pattern(name) => Path.explode(name) }) - .getOrElse(error("Failed to guess resulting .vsix file name")) - File.Content(path, Bytes.read(build_dir + path)) - }) + Isabelle_System.copy_file(build_dir + Path.basic(vsix_name), component_dir) + vsix_name + }) + + + /* settings */ + + val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) + File.write(etc_dir + Path.basic("settings"), + """# -*- shell-script -*- :mode=shellscript: + +ISABELLE_VSCODE_VSIX="$COMPONENT/""" + vsix_name + "\"\n") + + + /* README */ + + File.write(component_dir + Path.basic("README"), + """This the Isabelle/VSCode extension as VSIX package + +It has been produced from the sources in $ISABELLE_HOME/src/Tools/extension/. + + + Makarius + """ + Date.Format.date(Date.now()) + "\n") } @@ -169,24 +204,22 @@ Isabelle_Tool("build_vscode_extension", "build Isabelle/VSCode extension module", Scala_Project.here, args => { + var target_dir = Path.current var dirs: List[Path] = Nil var logic = default_logic - var install = false - var uninstall = false val getopts = Getopts(""" Usage: isabelle build_vscode_extension Options are: - -I install resulting extension - -U uninstall extension (no build) + -D DIR target directory (default ".") -d DIR include session directory -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) -Build Isabelle/VSCode extension module (vsix). +Build the Isabelle/VSCode extension as component, for inclusion into the +local VSCodium configuration. """, - "I" -> (_ => install = true), - "U" -> (_ => uninstall = true), + "D:" -> (arg => target_dir = Path.explode(arg)), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "l:" -> (arg => logic = arg)) @@ -196,11 +229,7 @@ val options = Options.init() val progress = new Console_Progress() - if (uninstall) VSCode_Main.uninstall_extension(progress = progress) - else { - val vsix = build_extension(options, logic = logic, dirs = dirs, progress = progress) - vsix.write(VSCode_Main.extension_dir) - if (install) VSCode_Main.install_extension(vsix, progress = progress) - } + build_extension(options, target_dir = target_dir, logic = logic, dirs = dirs, + progress = progress) }) } diff -r c3f1bf2824bc -r 4598cf29ef98 src/Tools/VSCode/src/vscode_main.scala --- a/src/Tools/VSCode/src/vscode_main.scala Thu Mar 24 22:43:41 2022 +0000 +++ b/src/Tools/VSCode/src/vscode_main.scala Thu Mar 24 23:54:40 2022 +0100 @@ -75,13 +75,16 @@ /* extension */ + def default_vsix_path: Path = Path.explode("$ISABELLE_VSCODE_VSIX") + def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension") + val extension_name: String = "isabelle.isabelle" def extension_manifest(): Manifest = new Manifest - val extension_name: String = "isabelle.isabelle" + + private val MANIFEST: Path = Path.explode("MANIFEST") final class Manifest private[VSCode_Main] { - private val MANIFEST: Path = Path.explode("MANIFEST") private val text = File.read(extension_dir + MANIFEST) private def entries: List[String] = split_lines(text).filter(_.nonEmpty) @@ -94,26 +97,6 @@ terminate_lines(a :: bs) } - def check_vsix(path: Path): Boolean = - { - path.is_file && { - using(new ZipFile(path.file))(zip_file => - { - val entry = zip_file.getEntry("extension/MANIFEST.shasum") - entry != null && { - val stream = zip_file.getInputStream(entry) - stream != null && File.read_stream(stream) == extension_manifest().shasum - } - }) - } - } - - def check_dir(dir: Path): Boolean = - { - val path = dir + MANIFEST.shasum - path.is_file && File.read(path) == shasum - } - def prepare_dir(dir: Path): Unit = { for (entry <- entries) { @@ -125,6 +108,30 @@ } } + private def shasum_vsix(vsix_path: Path): String = + { + val name = "extension/MANIFEST.shasum" + def err(): Nothing = error("Cannot retrieve " + quote(name) + " from " + vsix_path) + if (vsix_path.is_file) { + using(new ZipFile(vsix_path.file))(zip_file => + zip_file.getEntry(name) match { + case null => err() + case entry => + zip_file.getInputStream(entry) match { + case null => err() + case stream => File.read_stream(stream) + } + }) + } + else err() + } + + private def shasum_dir(dir: Path): Option[String] = + { + val path = dir + MANIFEST.shasum + if (path.is_file) Some(File.read(path)) else None + } + def locate_extension(): Option[Path] = { val out = run_vscodium(List("--locate-extension", extension_name)).check.out @@ -133,26 +140,35 @@ def uninstall_extension(progress: Progress = new Progress): Unit = locate_extension() match { - case None => progress.echo_warning("No extension " + quote(extension_name) + " to uninstall") + case None => progress.echo_warning("No Isabelle/VSCode extension to uninstall") case Some(dir) => run_vscodium(List("--uninstall-extension", extension_name)).check - progress.echo("Uninstalled extension " + quote(extension_name) + - " from directory:\n " + dir) + progress.echo("Uninstalled Isabelle/VSCode extension from directory:\n" + dir) } - def install_extension(vsix: File.Content, progress: Progress = new Progress): Unit = + def install_extension( + vsix_path: Path = default_vsix_path, + progress: Progress = new Progress): Unit = { - Isabelle_System.with_tmp_dir("tmp")(tmp_dir => - { - vsix.write(tmp_dir) - run_vscodium(List("--install-extension", File.platform_path(tmp_dir + vsix.path))).check + val new_shasum = shasum_vsix(vsix_path) + val old_shasum = locate_extension().flatMap(shasum_dir) + val current = old_shasum.isDefined && old_shasum.get == new_shasum + + if (!current) { + run_vscodium(List("--install-extension", File.bash_platform_path(vsix_path))).check locate_extension() match { - case None => error("No extension " + extension_name + " after installation") + case None => error("Missing Isabelle/VSCode extension after installation") case Some(dir) => - progress.echo("Installed extension " + quote(extension_name) + - " into directory:\n " + dir) + progress.echo("Installed Isabelle/VSCode extension " + vsix_path.expand + + "\ninto directory: " + dir) } - }) + val manifest = extension_manifest() + if (manifest.shasum != new_shasum) { + progress.echo_warning( + "Isabelle/VSCode extension " + vsix_path.expand + + "\ndisagrees with project sources" + extension_dir.expand) + } + } } @@ -191,8 +207,11 @@ { var logic_ancestor = "" var console = false + var edit_extension = false var server_log = false var logic_requirements = false + var uninstall = false + var vsix_path = default_vsix_path var session_dirs = List.empty[Path] var include_sessions = List.empty[String] var logic = "" @@ -208,9 +227,13 @@ -A NAME ancestor session for option -R (default: parent) -C run as foreground process, with console output + -E edit Isabelle/VSCode extension project sources -L enable language server log to file: """ + server_log_path.implode + """ -R NAME build image with requirements from other sessions + -U uninstall Isabelle/VSCode extension + -V FILE specify VSIX file for Isabelle/VSCode extension + (default: """ + default_vsix_path + """) -d DIR include session directory -i NAME include session in name-space of theories -l NAME logic session name @@ -229,8 +252,11 @@ """ + default_settings, "A:" -> (arg => logic_ancestor = arg), "C" -> (_ => console = true), + "E" -> (_ => edit_extension = true), "L" -> (_ => server_log = true), "R:" -> (arg => { logic = arg; logic_requirements = true }), + "U" -> (_ => uninstall = true), + "V" -> (arg => vsix_path = Path.explode(arg)), "d:" -> (arg => session_dirs = session_dirs ::: List(Path.explode(arg))), "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), "l:" -> (arg => { logic = arg; logic_requirements = false }), @@ -246,14 +272,21 @@ init_settings() - val (background, progress) = - if (console) (false, new Console_Progress) + val console_progress = new Console_Progress + + if (uninstall) uninstall_extension(progress = console_progress) + else install_extension(vsix_path = vsix_path, progress = console_progress) + + val (background, app_progress) = + if (console) (false, console_progress) else { run_vscodium(List("--version")).check; (true, new Progress) } - run_vscodium(more_args, options = options, logic = logic, logic_ancestor = logic_ancestor, + run_vscodium( + more_args ::: (if (edit_extension) List(File.platform_path(extension_dir)) else Nil), + options = options, logic = logic, logic_ancestor = logic_ancestor, logic_requirements = logic_requirements, session_dirs = session_dirs, include_sessions = include_sessions, modes = modes, no_build = no_build, server_log = server_log, verbose = verbose, background = background, - progress = progress).check + progress = app_progress).check }) }