# HG changeset patch # User wenzelm # Date 1648063593 -3600 # Node ID 8fcf5770863633951f662de545f2ac901764e783 # Parent c8a9bf6d9b389c9ca585c05f85add36080067616# Parent d7f41034a239c23ef83273b98bc01b89b627cecf merged diff -r c8a9bf6d9b38 -r 8fcf57708636 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Wed Mar 23 14:36:11 2022 +0000 +++ b/Admin/components/components.sha1 Wed Mar 23 20:26:33 2022 +0100 @@ -148,6 +148,7 @@ 309909ec6d43ae460338e9af54c1b2a48adcb1ec isabelle_setup-20210726.tar.gz a14ce46c62c64c3413f3cc9239242e33570d0f3d isabelle_setup-20210922.tar.gz b22066a9dcde6f813352dcf6404ac184440a22df isabelle_setup-20211109.tar.gz +91c5d29e9fa40aee015e8e65ffea043e218c2fc5 isabelle_setup-20220323.tar.gz 0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz 3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz diff -r c8a9bf6d9b38 -r 8fcf57708636 Admin/components/main --- a/Admin/components/main Wed Mar 23 14:36:11 2022 +0000 +++ b/Admin/components/main Wed Mar 23 20:26:33 2022 +0100 @@ -9,7 +9,7 @@ flatlaf-1.6.4 idea-icons-20210508 isabelle_fonts-20211004 -isabelle_setup-20211109 +isabelle_setup-20220323 jdk-17.0.2+8 jedit-20211103 jfreechart-1.5.3 diff -r c8a9bf6d9b38 -r 8fcf57708636 Admin/lib/Tools/build_setup --- a/Admin/lib/Tools/build_setup Wed Mar 23 14:36:11 2022 +0000 +++ b/Admin/lib/Tools/build_setup Wed Mar 23 20:26:33 2022 +0100 @@ -11,7 +11,7 @@ function usage() { echo - echo "Usage: isabelle $PRG [OPTIONS] COMPONENT_DIR" + echo "Usage: isabelle $PRG COMPONENT_DIR" echo echo " Build component for Isabelle/Java setup tool." echo diff -r c8a9bf6d9b38 -r 8fcf57708636 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Wed Mar 23 14:36:11 2022 +0000 +++ b/src/Pure/General/path.scala Wed Mar 23 20:26:33 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 c8a9bf6d9b38 -r 8fcf57708636 src/Pure/General/sha1.scala --- a/src/Pure/General/sha1.scala Wed Mar 23 14:36:11 2022 +0000 +++ b/src/Pure/General/sha1.scala Wed Mar 23 20:26:33 2022 +0100 @@ -1,7 +1,7 @@ /* Title: Pure/General/sha1.scala Author: Makarius -Digest strings according to SHA-1 (see RFC 3174). +SHA-1 message digest according to RFC 3174. */ package isabelle @@ -10,64 +10,47 @@ import java.io.{File => JFile, FileInputStream} import java.security.MessageDigest +import isabelle.setup.{Build => Setup_Build} + object SHA1 { - final class Digest private[SHA1](val rep: String) + final class Digest private[SHA1](rep: String) { + override def toString: String = rep override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { - case other: Digest => rep == other.rep + case other: Digest => rep == other.toString case _ => false } - override def toString: String = rep } - private def make_result(digest: MessageDigest): Digest = + def fake_digest(rep: String): Digest = new Digest(rep) + + def make_digest(body: MessageDigest => Unit): Digest = { - val result = new StringBuilder - for (b <- digest.digest()) { - val i = b.asInstanceOf[Int] & 0xFF - if (i < 16) result += '0' - result ++= Integer.toHexString(i) - } - new Digest(result.toString) + val digest_body = new Setup_Build.Digest_Body { def apply(sha: MessageDigest): Unit = body(sha)} + new Digest(Setup_Build.make_digest(digest_body)) } - def fake(rep: String): Digest = new Digest(rep) - def digest(file: JFile): Digest = - { - val digest = MessageDigest.getInstance("SHA") - - using(new FileInputStream(file))(stream => - { - val buf = new Array[Byte](65536) - var m = 0 - do { - m = stream.read(buf, 0, buf.length) - if (m != -1) digest.update(buf, 0, m) - } while (m != -1) - }) - - make_result(digest) - } + make_digest(sha => using(new FileInputStream(file))(stream => + { + val buf = new Array[Byte](65536) + var m = 0 + do { + m = stream.read(buf, 0, buf.length) + if (m != -1) sha.update(buf, 0, m) + } while (m != -1) + })) def digest(path: Path): Digest = digest(path.file) - - def digest(bytes: Array[Byte]): Digest = - { - val digest = MessageDigest.getInstance("SHA") - digest.update(bytes) - - make_result(digest) - } - + def digest(bytes: Array[Byte]): Digest = make_digest(_.update(bytes)) def digest(bytes: Bytes): Digest = bytes.sha1_digest def digest(string: String): Digest = digest(Bytes(string)) def digest_set(digests: List[Digest]): Digest = digest(cat_lines(digests.map(_.toString).sorted)) - val digest_length: Int = digest("").rep.length + val digest_length: Int = digest("").toString.length } diff -r c8a9bf6d9b38 -r 8fcf57708636 src/Pure/System/components.scala --- a/src/Pure/System/components.scala Wed Mar 23 14:36:11 2022 +0000 +++ b/src/Pure/System/components.scala Wed Mar 23 20:26:33 2022 +0100 @@ -303,8 +303,7 @@ yield { val file_name = archive.file_name progress.echo("Digesting local " + file_name) - val sha1 = SHA1.digest(archive).rep - SHA1_Digest(sha1, file_name) + SHA1_Digest(SHA1.digest(archive).toString, file_name) } val new_names = new_entries.map(_.file_name).toSet diff -r c8a9bf6d9b38 -r 8fcf57708636 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Wed Mar 23 14:36:11 2022 +0000 +++ b/src/Pure/Thy/document_build.scala Wed Mar 23 20:26:33 2022 +0100 @@ -81,7 +81,7 @@ { val name = res.string(Data.name) val sources = res.string(Data.sources) - Document_Input(name, SHA1.fake(sources)) + Document_Input(name, SHA1.fake_digest(sources)) }).toList) } @@ -96,7 +96,7 @@ val sources = res.string(Data.sources) val log_xz = res.bytes(Data.log_xz) val pdf = res.bytes(Data.pdf) - Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf)) + Some(Document_Output(name, SHA1.fake_digest(sources), log_xz, pdf)) } else None }) diff -r c8a9bf6d9b38 -r 8fcf57708636 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Mar 23 14:36:11 2022 +0000 +++ b/src/Pure/Thy/sessions.scala Wed Mar 23 20:26:33 2022 +0100 @@ -1172,7 +1172,7 @@ def write_heap_digest(heap: Path): String = read_heap_digest(heap) match { case None => - val s = SHA1.digest(heap).rep + val s = SHA1.digest(heap).toString File.append(heap, sha1_prefix + s) s case Some(s) => s diff -r c8a9bf6d9b38 -r 8fcf57708636 src/Tools/Setup/src/Build.java --- a/src/Tools/Setup/src/Build.java Wed Mar 23 14:36:11 2022 +0000 +++ b/src/Tools/Setup/src/Build.java Wed Mar 23 20:26:33 2022 +0100 @@ -8,7 +8,6 @@ import java.io.BufferedOutputStream; -import java.io.ByteArrayOutputStream; import java.io.CharArrayWriter; import java.io.File; import java.io.IOException; @@ -44,6 +43,30 @@ public class Build { + /** SHA1 digest **/ + + @FunctionalInterface + public interface Digest_Body + { + void apply(MessageDigest sha) throws IOException, InterruptedException; + } + + public static String make_digest(Digest_Body body) + throws NoSuchAlgorithmException, IOException, InterruptedException + { + MessageDigest sha = MessageDigest.getInstance("SHA"); + body.apply(sha); + return String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())); + } + + public static String make_shasum(String name, Digest_Body body) + throws NoSuchAlgorithmException, IOException, InterruptedException + { + return make_digest(body) + " " + name + "\n"; + } + + + /** context **/ public static String BUILD_PROPS = "build.props"; @@ -77,12 +100,6 @@ return List.copyOf(result); } - private static String sha_digest(MessageDigest sha, String name) - { - String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())); - return digest + " " + name + "\n"; - } - public static class Context { private final Path _dir; @@ -181,37 +198,37 @@ } public String shasum(String name, List paths) - throws IOException, NoSuchAlgorithmException + throws NoSuchAlgorithmException, IOException, InterruptedException { - MessageDigest sha = MessageDigest.getInstance("SHA"); - for (Path file : paths) { - if (Files.isRegularFile(file)) { - sha.update(Files.readAllBytes(file)); - } - else { - throw new RuntimeException( - error_message("Bad input file " + Library.quote(file.toString()))); - } - } - return sha_digest(sha, name); + return make_shasum(name, sha -> + { + for (Path file : paths) { + if (Files.isRegularFile(file)) { + sha.update(Files.readAllBytes(file)); + } + else { + throw new RuntimeException( + error_message("Bad input file " + Library.quote(file.toString()))); + } + } + }); } public String shasum(String file) - throws IOException, NoSuchAlgorithmException, InterruptedException + throws NoSuchAlgorithmException, IOException, InterruptedException { return shasum(file, List.of(path(file))); } public String shasum_props() - throws NoSuchAlgorithmException + throws NoSuchAlgorithmException, IOException, InterruptedException { TreeMap sorted = new TreeMap(); for (Object x : _props.entrySet()) { sorted.put(x.toString(), _props.get(x)); } - MessageDigest sha = MessageDigest.getInstance("SHA"); - sha.update(sorted.toString().getBytes(StandardCharsets.UTF_8)); - return sha_digest(sha, ""); + return make_shasum("", + sha -> sha.update(sorted.toString().getBytes(StandardCharsets.UTF_8))); } } @@ -423,7 +440,7 @@ /** build **/ public static void build(PrintStream output, Context context, boolean fresh) - throws IOException, InterruptedException, NoSuchAlgorithmException + throws NoSuchAlgorithmException, IOException, InterruptedException { String module = context.module_result(); if (!module.isEmpty()) { @@ -532,7 +549,7 @@ } public static void build_components(PrintStream output, boolean fresh) - throws IOException, InterruptedException, NoSuchAlgorithmException + throws NoSuchAlgorithmException, IOException, InterruptedException { for (Context context : component_contexts()) { build(output, context, fresh); diff -r c8a9bf6d9b38 -r 8fcf57708636 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Wed Mar 23 14:36:11 2022 +0000 +++ b/src/Tools/VSCode/extension/package.json Wed Mar 23 20:26:33 2022 +0100 @@ -11,7 +11,7 @@ ], "icon": "isabelle.png", "version": "2.0.0", - "publisher": "Isabelle", + "publisher": "isabelle", "license": "MIT", "repository": { "url": "https://isabelle-dev.sketis.net" diff -r c8a9bf6d9b38 -r 8fcf57708636 src/Tools/VSCode/src/build_vscode_extension.scala --- a/src/Tools/VSCode/src/build_vscode_extension.scala Wed Mar 23 14:36:11 2022 +0000 +++ b/src/Tools/VSCode/src/build_vscode_extension.scala Wed Mar 23 20:26:33 2022 +0100 @@ -135,23 +135,7 @@ } - /* extension */ - - lazy val extension_dir = Path.explode("$ISABELLE_VSCODE_HOME/extension") - - def uninstall_extension(progress: Progress = new Progress): Unit = - VSCode_Main.run_cli( - List("--uninstall-extension", "Isabelle.isabelle"), progress = progress).check - - def install_extension(vsix: File.Content, progress: Progress = new Progress): Unit = - { - Isabelle_System.with_tmp_dir("tmp")(tmp_dir => - { - vsix.write(tmp_dir) - VSCode_Main.run_cli( - List("--install-extension", File.platform_path(tmp_dir + vsix.path)), progress = progress).check - }) - } + /* build extension */ def build_extension(options: Options, logic: String = default_logic, @@ -164,14 +148,7 @@ Isabelle_System.with_tmp_dir("build")(build_dir => { - for { - line <- split_lines(File.read(extension_dir + Path.explode("MANIFEST"))) - if line.nonEmpty - } { - val path = Path.explode(line) - Isabelle_System.copy_file(extension_dir + path, - Isabelle_System.make_directory(build_dir + path.dir)) - } + VSCode_Main.extension_manifest().prepare_dir(build_dir) build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress) @@ -219,11 +196,11 @@ val options = Options.init() val progress = new Console_Progress() - if (uninstall) uninstall_extension(progress = progress) + if (uninstall) VSCode_Main.uninstall_extension(progress = progress) else { val vsix = build_extension(options, logic = logic, dirs = dirs, progress = progress) - vsix.write(extension_dir) - if (install) install_extension(vsix, progress = progress) + vsix.write(VSCode_Main.extension_dir) + if (install) VSCode_Main.install_extension(vsix, progress = progress) } }) } diff -r c8a9bf6d9b38 -r 8fcf57708636 src/Tools/VSCode/src/vscode_main.scala --- a/src/Tools/VSCode/src/vscode_main.scala Wed Mar 23 14:36:11 2022 +0000 +++ b/src/Tools/VSCode/src/vscode_main.scala Wed Mar 23 20:26:33 2022 +0100 @@ -9,17 +9,17 @@ import isabelle._ +import java.util.zip.ZipFile + object VSCode_Main { /* vscodium command-line interface */ - private def platform_path(s: String): String = File.platform_path(Path.explode(s)) - def server_log_path: Path = Path.explode("$ISABELLE_VSCODE_SETTINGS/server.log").expand - def run_cli(args: List[String], + def run_vscodium(args: List[String], environment: Iterable[(String, String)] = Nil, options: List[String] = Nil, logic: String = "", @@ -34,6 +34,8 @@ background: Boolean = false, progress: Progress = new Progress): Process_Result = { + def platform_path(s: String): String = File.platform_path(Path.explode(s)) + val args_json = JSON.optional("options" -> proper_list(options)) ++ JSON.optional("logic" -> proper_string(logic)) ++ @@ -71,6 +73,89 @@ } + /* extension */ + + def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension") + def extension_manifest(): Manifest = new Manifest + val extension_name: String = "isabelle.isabelle" + + 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_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) { + 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 locate_extension(): Option[Path] = + { + val out = run_vscodium(List("--locate-extension", extension_name)).check.out + if (out.nonEmpty) Some(Path.explode(File.standard_path(out))) else None + } + + def uninstall_extension(progress: Progress = new Progress): Unit = + locate_extension() match { + case None => progress.echo_warning("No extension " + quote(extension_name) + " to uninstall") + case Some(dir) => + run_vscodium(List("--uninstall-extension", extension_name)).check + progress.echo("Uninstalled extension " + quote(extension_name) + + " from directory:\n " + dir) + } + + def install_extension(vsix: File.Content, 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 + locate_extension() match { + case None => error("No extension " + extension_name + " after installation") + case Some(dir) => + progress.echo("Installed extension " + quote(extension_name) + + " into directory:\n " + dir) + } + }) + } + + /* settings */ def settings_path: Path = @@ -119,7 +204,7 @@ def add_option(opt: String): Unit = options = options ::: List(opt) val getopts = Getopts(""" -Usage: isabelle vscode [OPTIONS] [-- VSCODE_OPTIONS ...] +Usage: isabelle vscode [OPTIONS] [ARGUMENTS] [-- VSCODE_OPTIONS] -A NAME ancestor session for option -R (default: parent) -C run as foreground process, with console output @@ -163,9 +248,9 @@ val (background, progress) = if (console) (false, new Console_Progress) - else { run_cli(List("--version")).check; (true, new Progress) } + else { run_vscodium(List("--version")).check; (true, new Progress) } - run_cli(more_args, options = options, logic = logic, logic_ancestor = logic_ancestor, + run_vscodium(more_args, 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,