# HG changeset patch # User wenzelm # Date 1648157237 -3600 # Node ID 8f0d94fb8551c37298ce9202ab273e81afaea99b # Parent 96a33aaf23a1e36b8165d09f4fb0b3aa02c1c14a provide vscode_extension via component, thus users don't need Node.js development tools; proper default for edit_extension; tuned messages; diff -r 96a33aaf23a1 -r 8f0d94fb8551 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Mar 24 20:45:14 2022 +0100 +++ b/Admin/components/components.sha1 Thu Mar 24 22:27:17 2022 +0100 @@ -446,6 +446,7 @@ 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 81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz diff -r 96a33aaf23a1 -r 8f0d94fb8551 Admin/components/main --- a/Admin/components/main Thu Mar 24 20:45:14 2022 +0100 +++ b/Admin/components/main Thu Mar 24 22:27:17 2022 +0100 @@ -29,6 +29,7 @@ stack-2.7.3 vampire-4.6 verit-2021.06.2-rmx +vscode_extension-20220324 xz-java-1.9 z3-4.4.0_4.4.1 zipperposition-2.1-1 diff -r 96a33aaf23a1 -r 8f0d94fb8551 src/Tools/VSCode/src/build_vscode_extension.scala --- a/src/Tools/VSCode/src/build_vscode_extension.scala Thu Mar 24 20:45:14 2022 +0100 +++ b/src/Tools/VSCode/src/build_vscode_extension.scala Thu Mar 24 22:27:17 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,21 +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 val getopts = Getopts(""" Usage: isabelle build_vscode_extension Options are: - -I install resulting extension + -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), + "D:" -> (arg => target_dir = Path.explode(arg)), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "l:" -> (arg => logic = arg)) @@ -193,8 +229,7 @@ val options = Options.init() val progress = new Console_Progress() - 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 96a33aaf23a1 -r 8f0d94fb8551 src/Tools/VSCode/src/vscode_main.scala --- a/src/Tools/VSCode/src/vscode_main.scala Thu Mar 24 20:45:14 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_main.scala Thu Mar 24 22:27:17 2022 +0100 @@ -75,13 +75,40 @@ /* extension */ + def default_vsix_path: Path = Path.explode("$ISABELLE_VSCODE_VSIX") + def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension") def extension_manifest(): Manifest = new Manifest val extension_name: String = "isabelle.isabelle" + private val MANIFEST: Path = Path.explode("MANIFEST") + + 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 => + { + val entry = zip_file.getEntry(name) + if (entry == null) err() + else { + val stream = zip_file.getInputStream(entry) + if (stream == null) err() else 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 + } + 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 +121,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) { @@ -136,21 +143,32 @@ 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 Isabelle/VSCode extension 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("Missing extension Isabelle/VSCode after installation") + case None => error("Missing Isabelle/VSCode extension after installation") case Some(dir) => - progress.echo("Installed Isabelle/VSCode extension 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) + } + } } @@ -189,10 +207,11 @@ { var logic_ancestor = "" var console = false - var edit_extension = true + 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 = "" @@ -213,6 +232,8 @@ """ + 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 @@ -235,6 +256,7 @@ "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 }), @@ -253,6 +275,7 @@ 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)