# HG changeset patch # User wenzelm # Date 1648037154 -3600 # Node ID e641ac92b489e868d72fd23a736020d8de390cd5 # Parent 5960bae73afe4907572a89cd73026af955ff12fd more formal extension_manifest, with shasum for sources; diff -r 5960bae73afe -r e641ac92b489 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Wed Mar 23 12:21:13 2022 +0100 +++ b/src/Pure/General/path.scala Wed Mar 23 13:05:54 2022 +0100 @@ -235,6 +235,7 @@ def log: Path = ext("log") def orig: Path = ext("orig") def patch: Path = ext("patch") + def shasum: Path = ext("shasum") def backup: Path = { diff -r 5960bae73afe -r e641ac92b489 src/Tools/VSCode/src/build_vscode_extension.scala --- a/src/Tools/VSCode/src/build_vscode_extension.scala Wed Mar 23 12:21:13 2022 +0100 +++ b/src/Tools/VSCode/src/build_vscode_extension.scala Wed Mar 23 13:05:54 2022 +0100 @@ -135,13 +135,7 @@ } - /* extension */ - - def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension") - def extension_manifest: Path = extension_dir + Path.explode("MANIFEST") - def manifest_entries(): List[Path] = - for (line <- split_lines(File.read(extension_manifest)) if line.nonEmpty) - yield Path.explode(line) + /* build extension */ def build_extension(options: Options, logic: String = default_logic, @@ -154,10 +148,7 @@ Isabelle_System.with_tmp_dir("build")(build_dir => { - for (path <- manifest_entries()) { - Isabelle_System.copy_file(extension_dir + path, - Isabelle_System.make_directory(build_dir + path.dir)) - } + VSCode_Main.extension_manifest().write(build_dir) build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress) @@ -208,7 +199,7 @@ if (uninstall) VSCode_Main.uninstall_extension(progress = progress) else { val vsix = build_extension(options, logic = logic, dirs = dirs, progress = progress) - vsix.write(extension_dir) + vsix.write(VSCode_Main.extension_dir) if (install) VSCode_Main.install_extension(vsix, progress = progress) } }) diff -r 5960bae73afe -r e641ac92b489 src/Tools/VSCode/src/vscode_main.scala --- a/src/Tools/VSCode/src/vscode_main.scala Wed Mar 23 12:21:13 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_main.scala Wed Mar 23 13:05:54 2022 +0100 @@ -71,7 +71,42 @@ } - /* extensions */ + /* extension */ + + def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension") + def extension_manifest(): Manifest = new 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) + + val shasum: String = + { + val a = SHA1.digest(text).toString + " " + val bs = + for (entry <- entries) + yield SHA1.digest(extension_dir + Path.explode(entry)).toString + " " + entry + terminate_lines(a :: bs) + } + + def check(dir: Path): Boolean = + { + val path = dir + MANIFEST.shasum + path.is_file && File.read(path) == shasum + } + + def write(dir: Path): Unit = + { + for (entry <- entries) { + val path = Path.explode(entry) + Isabelle_System.copy_file(extension_dir + path, + Isabelle_System.make_directory(dir + path.dir)) + } + File.write(dir + MANIFEST.shasum, shasum) + } + } def uninstall_extension(progress: Progress = new Progress): Unit = run_vscodium(List("--uninstall-extension", "Isabelle.isabelle"), progress = progress).check