# HG changeset patch
# User wenzelm
# Date 1675692261 -3600
# Node ID a3f67a4459e1b00b2149c1d764dac8c848f3b2b7
# Parent  d98a99e4eea94f91ee715f91e91ca5da1e65e8e7
more uniform use of SHA1.Shasum;

diff -r d98a99e4eea9 -r a3f67a4459e1 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Feb 06 14:54:15 2023 +0100
+++ b/Admin/components/components.sha1	Mon Feb 06 15:04:21 2023 +0100
@@ -494,6 +494,7 @@
 c4666a6d8080b5e376b50471fd2d9edeb1f9c988 vscode_extension-20220324.tar.gz
 86c952d739d1eb868be88898982d4870a3d8c2dc vscode_extension-20220325.tar.gz
 5293b9e77e5c887d449b671828b133fad4f18632 vscode_extension-20220829.tar.gz
+0d9551ffeb968813b6017278fa7ab9bd6062883f vscode_extension-20230206.tar.gz
 67b271186631f84efd97246bf85f6d8cfaa5edfd vscodium-1.65.2.tar.gz
 c439ab741e0cc49354cc03aa9af501202a5a38e3 vscodium-1.70.1.tar.gz
 81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz
diff -r d98a99e4eea9 -r a3f67a4459e1 Admin/components/main
--- a/Admin/components/main	Mon Feb 06 14:54:15 2023 +0100
+++ b/Admin/components/main	Mon Feb 06 15:04:21 2023 +0100
@@ -35,7 +35,7 @@
 stack-2.7.3
 vampire-4.6
 verit-2021.06.2-rmx
-vscode_extension-20220829
+vscode_extension-20230206
 vscodium-1.70.1
 xz-java-1.9
 z3-4.4.0_4.4.1
diff -r d98a99e4eea9 -r a3f67a4459e1 src/Tools/VSCode/src/build_vscode_extension.scala
--- a/src/Tools/VSCode/src/build_vscode_extension.scala	Mon Feb 06 14:54:15 2023 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala	Mon Feb 06 15:04:21 2023 +0100
@@ -160,19 +160,19 @@
       Isabelle_System.with_tmp_dir("build") { build_dir =>
         val manifest_text = File.read(VSCode_Main.extension_dir + VSCode_Main.MANIFEST)
         val manifest_entries = split_lines(manifest_text).filter(_.nonEmpty)
-        val manifest_shasum: String = {
-          val a = SHA1.digest(manifest_text).shasum("<MANIFEST>")
+        val manifest_shasum: SHA1.Shasum = {
+          val a = SHA1.shasum_meta_info(SHA1.digest(manifest_text))
           val bs =
-            for (entry <- manifest_entries)
-              yield SHA1.digest(VSCode_Main.extension_dir + Path.explode(entry)).shasum(entry)
-          terminate_lines(a :: bs)
+            for (name <- manifest_entries)
+              yield SHA1.shasum(SHA1.digest(VSCode_Main.extension_dir + Path.explode(name)), name)
+          SHA1.flat_shasum(a :: bs)
         }
-        for (entry <- manifest_entries) {
-          val path = Path.explode(entry)
+        for (name <- manifest_entries) {
+          val path = Path.explode(name)
           Isabelle_System.copy_file(VSCode_Main.extension_dir + path,
             Isabelle_System.make_directory(build_dir + path.dir))
         }
-        File.write(build_dir + VSCode_Main.MANIFEST.shasum, manifest_shasum)
+        File.write(build_dir + VSCode_Main.MANIFEST.shasum, manifest_shasum.toString)
 
         build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress)
 
diff -r d98a99e4eea9 -r a3f67a4459e1 src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Mon Feb 06 14:54:15 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala	Mon Feb 06 15:04:21 2023 +0100
@@ -81,7 +81,7 @@
 
   val MANIFEST: Path = Path.explode("MANIFEST")
 
-  private def shasum_vsix(vsix_path: Path): String = {
+  private def shasum_vsix(vsix_path: Path): SHA1.Shasum = {
     val name = "extension/MANIFEST.shasum"
     def err(): Nothing = error("Cannot retrieve " + quote(name) + " from " + vsix_path)
     if (vsix_path.is_file) {
@@ -91,16 +91,16 @@
           case entry =>
             zip_file.getInputStream(entry) match {
               case null => err()
-              case stream => File.read_stream(stream)
+              case stream => SHA1.fake_shasum(File.read_stream(stream))
             }
         })
     }
     else err()
   }
 
-  private def shasum_dir(dir: Path): Option[String] = {
+  private def shasum_dir(dir: Path): Option[SHA1.Shasum] = {
     val path = dir + MANIFEST.shasum
-    if (path.is_file) Some(File.read(path)) else None
+    if (path.is_file) Some(SHA1.fake_shasum(File.read(path))) else None
   }
 
   def locate_extension(): Option[Path] = {