more formal extension_manifest, with shasum for sources;

--- 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 =
   {

--- 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)
       }
     })

--- 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 + " <MANIFEST>"
+      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