--- 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
--- 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
--- 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
--- 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 =
{
--- 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
}
--- 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
--- 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
})
--- 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
--- 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<Path> 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<String,Object> sorted = new TreeMap<String,Object>();
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, "<props>");
+ return make_shasum("<props>",
+ 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);
--- 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"
--- 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)
}
})
}
--- 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 + " <MANIFEST>"
+ 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,