# HG changeset patch
# User wenzelm
# Date 1648224012 -3600
# Node ID 583ad7a9941cd48503e5af13cec83b4ada8ff456
# Parent  b75fefe1ddb5960124a7fb53ea92443b1f1daea4
tuned signature;
clarified modules;

diff -r b75fefe1ddb5 -r 583ad7a9941c src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Fri Mar 25 16:41:03 2022 +0100
+++ b/src/Pure/General/sha1.scala	Fri Mar 25 17:00:12 2022 +0100
@@ -24,6 +24,7 @@
         case other: Digest => rep == other.toString
         case _ => false
       }
+    def shasum(name: String): String = rep + " " + name
   }
 
   def fake_digest(rep: String): Digest = new Digest(rep)
diff -r b75fefe1ddb5 -r 583ad7a9941c src/Tools/VSCode/src/build_vscode_extension.scala
--- a/src/Tools/VSCode/src/build_vscode_extension.scala	Fri Mar 25 16:41:03 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala	Fri Mar 25 17:00:12 2022 +0100
@@ -160,7 +160,22 @@
     val vsix_name =
       Isabelle_System.with_tmp_dir("build")(build_dir =>
       {
-        VSCode_Main.extension_manifest().prepare_dir(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 bs =
+            for (entry <- manifest_entries)
+              yield SHA1.digest(VSCode_Main.extension_dir + Path.explode(entry)).shasum(entry)
+          terminate_lines(a :: bs)
+        }
+        for (entry <- manifest_entries) {
+          val path = Path.explode(entry)
+          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)
 
         build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress)
 
diff -r b75fefe1ddb5 -r 583ad7a9941c src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Fri Mar 25 16:41:03 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala	Fri Mar 25 17:00:12 2022 +0100
@@ -79,34 +79,8 @@
 
   def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension")
   val extension_name: String = "isabelle.isabelle"
-  def extension_manifest(): Manifest = new Manifest
 
-  private val MANIFEST: Path = Path.explode("MANIFEST")
-
-  final class Manifest private[VSCode_Main]
-  {
-    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 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)
-    }
-  }
+  val MANIFEST: Path = Path.explode("MANIFEST")
 
   private def shasum_vsix(vsix_path: Path): String =
   {