# HG changeset patch
# User wenzelm
# Date 1675715542 -3600
# Node ID 35a05e61c7b430eaa13d47f273f035714333630f
# Parent  8f2e6186408f742cad316846deb482f0d7bdaf18# Parent  a10161fbc6deb0286e8fe7ca8c1beeaf65eb6013
merged

diff -r 8f2e6186408f -r 35a05e61c7b4 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Feb 06 15:41:23 2023 +0000
+++ b/Admin/components/components.sha1	Mon Feb 06 21:32:22 2023 +0100
@@ -164,6 +164,7 @@
 171df3eb58bdac4cc495f773b797fa578f7d4be6 isabelle_setup-20220817.tar.gz
 7b1ce9bd85e33076fa7022eeb66ce15915d078d9 isabelle_setup-20221020.tar.gz
 cb9f061ccd7c6f90d00c8aa115aeea8679f3f996 isabelle_setup-20221028.tar.gz
+f582c621471583d06e00007c6acc01376c7395af isabelle_setup-20230206.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
 e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
 3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
@@ -493,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 8f2e6186408f -r 35a05e61c7b4 Admin/components/main
--- a/Admin/components/main	Mon Feb 06 15:41:23 2023 +0000
+++ b/Admin/components/main	Mon Feb 06 21:32:22 2023 +0100
@@ -12,7 +12,7 @@
 foiltex-2.1.4b
 idea-icons-20210508
 isabelle_fonts-20211004
-isabelle_setup-20221028
+isabelle_setup-20230206
 jdk-17.0.6
 jedit-20211103
 jfreechart-1.5.3
@@ -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 8f2e6186408f -r 35a05e61c7b4 etc/settings
--- a/etc/settings	Mon Feb 06 15:41:23 2023 +0000
+++ b/etc/settings	Mon Feb 06 21:32:22 2023 +0100
@@ -66,6 +66,7 @@
 isabelle_directory '~'
 isabelle_directory '$ISABELLE_HOME_USER'
 isabelle_directory '~~'
+isabelle_directory '$ISABELLE_COMPONENTS_BASE'
 
 ISABELLE_COMPONENT_REPOSITORY="https://isabelle.sketis.net/components"
 ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib"
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Admin/build_history.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -295,8 +295,8 @@
 
               val session_sources =
                 store.read_build(db, session_name).map(_.sources) match {
-                  case Some(sources) if sources.length == SHA1.digest_length =>
-                    List("Sources " + session_name + " " + sources)
+                  case Some(sources) if !sources.is_empty =>
+                    List("Sources " + session_name + " " + sources.digest.toString)
                   case _ => Nil
                 }
 
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/General/file.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -55,8 +55,7 @@
   /* symbolic path representation, e.g. "~~/src/Pure/ROOT.ML" */
 
   def symbolic_path(path: Path): String = {
-    val directories =
-      Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
+    val directories = space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
     val full_name = standard_path(path)
     directories.view.flatMap(a =>
       try {
@@ -75,10 +74,7 @@
   /* platform files */
 
   def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile
-  def absolute_name(file: JFile): String = absolute(file).getPath
-
   def canonical(file: JFile): JFile = file.getCanonicalFile
-  def canonical_name(file: JFile): String = canonical(file).getPath
 
   def path(file: JFile): Path = Path.explode(standard_path(file))
   def path(java_path: JPath): Path = path(java_path.toFile)
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/General/mercurial.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -248,7 +248,7 @@
 
     def tags(rev: String = "tip"): String = {
       val result = identify(rev, options = "-t")
-      Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
+      space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
     }
 
     def paths(args: String = "", options: String = ""): List[String] =
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/General/sha1.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -14,6 +14,8 @@
 
 
 object SHA1 {
+  /* digest */
+
   final class Digest private[SHA1](rep: String) {
     override def toString: String = rep
     override def hashCode: Int = rep.hashCode
@@ -22,7 +24,6 @@
         case other: Digest => rep == other.toString
         case _ => false
       }
-    def shasum(name: String): String = rep + " " + name
   }
 
   def fake_digest(rep: String): Digest = new Digest(rep)
@@ -47,8 +48,42 @@
   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("").toString.length
+
+
+  /* shasum */
+
+  final class Shasum private[SHA1](private[SHA1] val rep: List[String]) {
+    override def equals(other: Any): Boolean =
+      other match {
+        case that: Shasum => rep.equals(that.rep)
+        case _ => false
+      }
+    override def hashCode: Int = rep.hashCode
+    override def toString: String = Library.terminate_lines(rep)
+
+    def is_empty: Boolean = rep.isEmpty
+
+    def :::(other: Shasum): Shasum = new Shasum(other.rep ::: rep)
+
+    def digest: Digest = {
+      rep match {
+        case List(s)
+        if s.length == digest_length && s.forall(Symbol.is_ascii_hex) => fake_digest(s)
+        case _ => SHA1.digest(toString)
+      }
+    }
+  }
+
+  val no_shasum: Shasum = new Shasum(Nil)
+  def flat_shasum(list: List[Shasum]): Shasum = new Shasum(list.flatMap(_.rep))
+  def fake_shasum(text: String): Shasum = new Shasum(Library.trim_split_lines(text))
+
+  def shasum(digest: Digest, name: String): Shasum =
+    new Shasum(List(digest.toString + " " + name))
+  def shasum_meta_info(digest: Digest): Shasum =
+    shasum(digest, isabelle.setup.Build.META_INFO)
+  def shasum_sorted(args: List[(Digest, String)]): Shasum =
+    flat_shasum(args.sortBy(_._2).map(shasum))
 }
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/ML/ml_heap.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -17,7 +17,7 @@
 
   private val sha1_prefix = "SHA1:"
 
-  def read_digest(heap: Path): Option[String] = {
+  def read_digest(heap: Path): Option[SHA1.Digest] = {
     if (heap.is_file) {
       using(FileChannel.open(heap.java_path, StandardOpenOption.READ)) { file =>
         val len = file.size
@@ -37,7 +37,7 @@
           if (i == n) {
             val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
             val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
-            if (prefix == sha1_prefix) Some(s) else None
+            if (prefix == sha1_prefix) Some(SHA1.fake_digest(s)) else None
           }
           else None
         }
@@ -47,10 +47,10 @@
     else None
   }
 
-  def write_digest(heap: Path): String =
+  def write_digest(heap: Path): SHA1.Digest =
     read_digest(heap) getOrElse {
-      val s = SHA1.digest(heap).toString
-      File.append(heap, sha1_prefix + s)
-      s
+      val digest = SHA1.digest(heap)
+      File.append(heap, sha1_prefix + digest.toString)
+      digest
     }
 }
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/ML/ml_statistics.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -54,7 +54,7 @@
     consume: Properties.T => Unit = Console.println
   ): Unit = {
     def progress_stdout(line: String): Unit = {
-      val props = Library.space_explode(',', line).flatMap(Properties.Eq.unapply)
+      val props = space_explode(',', line).flatMap(Properties.Eq.unapply)
       if (props.nonEmpty) consume(props)
     }
 
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/PIDE/document_editor.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -17,8 +17,8 @@
   def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output")
   def document_output(name: String): Path = document_output_dir() + Path.basic(name)
 
-  object Meta_Data {
-    def read(name: String = document_name): Option[Meta_Data] = {
+  object Meta_Info {
+    def read(name: String = document_name): Option[Meta_Info] = {
       val json_path = document_output(name).json
       if (json_path.is_file) {
         val json = JSON.parse(File.read(json_path))
@@ -28,7 +28,7 @@
           log <- JSON.string(json, "log")
           pdf <- JSON.string(json, "pdf")
         } yield {
-          Meta_Data(name,
+          Meta_Info(name,
             SortedSet.from(selection),
             SHA1.fake_digest(sources),
             SHA1.fake_digest(log),
@@ -53,7 +53,7 @@
     }
   }
 
-  sealed case class Meta_Data(
+  sealed case class Meta_Info(
     name: String,
     selection: SortedSet[String],
     sources: SHA1.Digest,
@@ -77,7 +77,7 @@
     val output = document_output(name)
     File.write(output.log, doc.log)
     Bytes.write(output.pdf, doc.pdf)
-    Meta_Data.write(selection, doc, name = name)
+    Meta_Info.write(selection, doc, name = name)
   }
 
   def view_document(name: String = document_name): Unit = {
@@ -171,9 +171,9 @@
       val variant = document_session.get_variant
       val directory = engine.prepare_directory(context, tmp_dir, variant, verbose = true)
       val ok =
-        Meta_Data.read() match {
-          case Some(meta_data) =>
-            meta_data.check_files() && meta_data.sources == directory.sources
+        Meta_Info.read() match {
+          case Some(meta_info) =>
+            meta_info.check_files() && meta_info.sources == directory.sources
           case None => false
         }
       if (!ok) {
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/System/components.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -217,19 +217,19 @@
 
   val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
 
-  sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) {
-    override def toString: String = digest.shasum(name)
+  sealed case class SHA1_Entry(digest: SHA1.Digest, name: String) {
+    override def toString: String = SHA1.shasum(digest, name).toString
   }
 
-  def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
+  def read_components_sha1(lines: List[String] = Nil): List[SHA1_Entry] =
     (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
       Word.explode(line) match {
         case Nil => None
-        case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name))
+        case List(sha1, name) => Some(SHA1_Entry(SHA1.fake_digest(sha1), name))
         case _ => error("Bad components.sha1 entry: " + quote(line))
       })
 
-  def write_components_sha1(entries: List[SHA1_Digest]): Unit =
+  def write_components_sha1(entries: List[SHA1_Entry]): Unit =
     File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n"))
 
 
@@ -243,7 +243,7 @@
 
   def write_components(lines: List[String]): Unit = {
     Isabelle_System.make_directory(components_path.dir)
-    File.write(components_path, Library.terminate_lines(lines))
+    File.write(components_path, terminate_lines(lines))
   }
 
   def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = {
@@ -384,7 +384,7 @@
         yield {
           val name = archive.file_name
           progress.echo("Digesting local " + name)
-          SHA1_Digest(SHA1.digest(archive), name)
+          SHA1_Entry(SHA1.digest(archive), name)
         }
       val new_names = new_entries.map(_.name).toSet
 
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/System/executable.scala
--- a/src/Pure/System/executable.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/System/executable.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -20,7 +20,7 @@
     val ldd_lines = {
       val ldd = if (Platform.is_macos) "otool -L" else "ldd"
       val script = mingw.bash_script(ldd + " " + File.bash_path(exe))
-      Library.split_lines(Isabelle_System.bash(script, cwd = exe_dir.file).check.out)
+      split_lines(Isabelle_System.bash(script, cwd = exe_dir.file).check.out)
     }
 
     def lib_name(lib: String): String =
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/System/isabelle_system.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -510,8 +510,7 @@
   def open_external_file(name: String): Boolean = {
     val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
     val external =
-      ext.nonEmpty &&
-      Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
+      ext.nonEmpty && space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
     if (external) {
       if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
       else open(name)
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Thy/bibtex.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -202,7 +202,7 @@
     override def toString: String = "Bibtex.Entries(" + entries.length + ")"
 
     def ::: (other: Entries): Entries =
-      new Entries(entries ::: other.entries, errors ::: other.errors)
+      new Entries(other.entries ::: entries, other.errors ::: errors)
   }
 
   object Session_Entries extends Scala.Fun("bibtex_session_entries") {
@@ -703,7 +703,7 @@
   /* cite commands */
 
   def cite_commands(options: Options): List[String] =
-    Library.space_explode(',', options.string("document_cite_commands"))
+    space_explode(',', options.string("document_cite_commands"))
 
   val CITE = "cite"
   val NOCITE = "nocite"
@@ -828,7 +828,7 @@
       val location =
         if (loc.startsWith("[") && loc.endsWith("]")) loc.substring(1, loc.length - 1)
         else loc
-      val citations = Library.space_explode(',', m.group(3)).map(_.trim)
+      val citations = space_explode(',', m.group(3)).map(_.trim)
       Regex.quoteReplacement(cite_antiquotation(name, location, citations))
     })
 
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Thy/browser_info.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -36,16 +36,16 @@
   }
 
 
-  /* meta data within the file-system */
+  /* meta info within the file-system */
 
-  object Meta_Data {
+  object Meta_Info {
     /* directory */
 
     val PATH: Path = Path.explode(".browser_info")
 
     def check_directory(dir: Path): Unit = {
       if (dir.is_dir && !(dir + PATH).is_dir && File.read_dir(dir).nonEmpty) {
-        error("Existing content in " + dir.expand + " lacks " + PATH + " meta data.\n" +
+        error("Existing content in " + dir.expand + " lacks " + PATH + " meta info.\n" +
           "To avoid potential disaster, it has not been changed automatically.\n" +
           "If this is the intended directory, please move/remove/empty it manually.")
       }
@@ -284,10 +284,10 @@
     /* maintain presentation structure */
 
     def update_chapter(session_name: String, session_description: String): Unit = synchronized {
-      val dir = Meta_Data.init_directory(chapter_dir(session_name))
-      Meta_Data.change(dir, Meta_Data.INDEX) { text =>
-        val index0 = Meta_Data.Index.parse(text, "chapter")
-        val item = Meta_Data.Item(session_name, description = session_description)
+      val dir = Meta_Info.init_directory(chapter_dir(session_name))
+      Meta_Info.change(dir, Meta_Info.INDEX) { text =>
+        val index0 = Meta_Info.Index.parse(text, "chapter")
+        val item = Meta_Info.Item(session_name, description = session_description)
         val index = index0 + item
 
         if (index != index0) {
@@ -311,17 +311,17 @@
     }
 
     def update_root(): Unit = synchronized {
-      Meta_Data.init_directory(root_dir)
+      Meta_Info.init_directory(root_dir)
       HTML.init_fonts(root_dir)
       Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
         root_dir + Path.explode("isabelle.gif"))
 
-      Meta_Data.change(root_dir, Meta_Data.INDEX) { text =>
-        val index0 = Meta_Data.Index.parse(text, "root")
+      Meta_Info.change(root_dir, Meta_Info.INDEX) { text =>
+        val index0 = Meta_Info.Index.parse(text, "root")
         val index = {
           val items1 =
             sessions_structure.known_chapters
-              .map(ch => Meta_Data.Item(ch.name, description = ch.description))
+              .map(ch => Meta_Info.Item(ch.name, description = ch.description))
           val items2 = index0.items.filterNot(item => items1.exists(_.name == item.name))
           index0.copy(items = items1 ::: items2)
         }
@@ -559,8 +559,8 @@
     val session_dir = context.session_dir(session_name).expand
     progress.echo("Presenting " + session_name + " in " + session_dir + " ...")
 
-    Meta_Data.init_directory(context.chapter_dir(session_name))
-    Meta_Data.clean_directory(session_dir)
+    Meta_Info.init_directory(context.chapter_dir(session_name))
+    Meta_Info.clean_directory(session_dir)
 
     val session = context.document_info.the_session(session_name)
 
@@ -662,7 +662,7 @@
           context.contents("Theories", theories),
         root = Some(context.root_dir))
 
-    Meta_Data.set_build_uuid(session_dir, session.build_uuid)
+    Meta_Info.set_build_uuid(session_dir, session.build_uuid)
 
     context.update_chapter(session_name, session_info.description)
   }
@@ -688,7 +688,7 @@
               case None => false
               case Some(build) =>
                 val session_dir = context0.session_dir(session_name)
-                !Meta_Data.check_build_uuid(session_dir, build.uuid)
+                !Meta_Info.check_build_uuid(session_dir, build.uuid)
             }
           }
         }
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Thy/document_build.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -19,7 +19,7 @@
 
   object Document_Variant {
     def parse(opt: String): Document_Variant =
-      Library.space_explode('=', opt) match {
+      space_explode('=', opt) match {
         case List(name) => Document_Variant(name, Latex.Tags.empty)
         case List(name, tags) => Document_Variant(name, Latex.Tags(tags))
         case _ => error("Malformed document variant: " + quote(opt))
@@ -30,10 +30,10 @@
     def print: String = if (tags.toString.isEmpty) name else name + "=" + tags.toString
   }
 
-  sealed case class Document_Input(name: String, sources: SHA1.Digest)
+  sealed case class Document_Input(name: String, sources: SHA1.Shasum)
   extends Document_Name { override def toString: String = name }
 
-  sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes)
+  sealed case class Document_Output(name: String, sources: SHA1.Shasum, log_xz: Bytes, pdf: Bytes)
   extends Document_Name {
     override def toString: String = name
 
@@ -74,7 +74,7 @@
       stmt.execute_query().iterator({ res =>
         val name = res.string(Data.name)
         val sources = res.string(Data.sources)
-        Document_Input(name, SHA1.fake_digest(sources))
+        Document_Input(name, SHA1.fake_shasum(sources))
       }).toList)
   }
 
@@ -91,7 +91,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_digest(sources), log_xz, pdf))
+        Some(Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf))
       }
       else None
     })
@@ -228,7 +228,7 @@
     lazy val session_tex: File.Content = {
       val path = Path.basic("session.tex")
       val content =
-        Library.terminate_lines(
+        terminate_lines(
           session_document_theories.map(name => "\\input{" + tex_name(name) + "}"))
       File.content(path, content)
     }
@@ -304,9 +304,16 @@
       val root_name1 = "root_" + doc.name
       val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"
 
-      val digests1 = List(doc.print, document_logo.toString, document_build).map(SHA1.digest)
-      val digests2 = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
-      val sources = SHA1.digest_set(digests1 ::: digests2)
+      val meta_info =
+        SHA1.shasum_meta_info(
+          SHA1.digest(List(doc.print, document_logo.toString, document_build).toString))
+
+      val manifest =
+        SHA1.shasum_sorted(
+          for (file <- File.find_files(doc_dir.file, follow_links = true))
+            yield SHA1.digest(file) -> File.path(doc_dir.java_path.relativize(file.toPath)).implode)
+
+      val sources = meta_info ::: manifest
 
 
       /* derived material: without SHA1 digest */
@@ -338,7 +345,7 @@
     doc_dir: Path,
     doc: Document_Variant,
     root_name: String,
-    sources: SHA1.Digest
+    sources: SHA1.Shasum
   ) {
     def root_name_script(ext: String = ""): String =
       Bash.string(if (ext.isEmpty) root_name else root_name + "." + ext)
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Thy/latex.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -99,8 +99,7 @@
 
     val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
 
-    private def explode(spec: String): List[String] =
-      Library.space_explode(',', spec)
+    private def explode(spec: String): List[String] = space_explode(',', spec)
 
     def apply(spec: String): Tags =
       new Tags(spec,
@@ -142,7 +141,7 @@
 \newcommand{\isafoldtag}[1]%
 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
 
-""" + Library.terminate_lines(tags))
+""" + terminate_lines(tags))
     }
   }
 
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Thy/sessions.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -142,6 +142,8 @@
       ", loaded_theories = " + loaded_theories.size +
       ", used_theories = " + used_theories.length
 
+    def all_sources: List[(Path, SHA1.Digest)] = imported_sources ::: session_sources
+
     def all_document_theories: List[Document.Node.Name] =
       proper_session_theories ::: document_theories
 
@@ -273,11 +275,14 @@
     def apply(name: String): Base = session_bases(name)
     def get(name: String): Option[Base] = session_bases.get(name)
 
-    def imported_sources(name: String): List[SHA1.Digest] =
-      session_bases(name).imported_sources.map(_._2)
-
-    def session_sources(name: String): List[SHA1.Digest] =
-      session_bases(name).session_sources.map(_._2)
+    def sources_shasum(name: String): SHA1.Shasum = {
+      val meta_info = SHA1.shasum_meta_info(sessions_structure(name).meta_digest)
+      val sources =
+        SHA1.shasum_sorted(
+          for ((path, digest) <- apply(name).all_sources)
+            yield digest -> File.symbolic_path(path))
+      meta_info ::: sources
+    }
 
     def errors: List[String] =
       (for {
@@ -684,7 +689,7 @@
 
     def document_variants: List[Document_Build.Document_Variant] = {
       val variants =
-        Library.space_explode(':', options.string("document_variants")).
+        space_explode(':', options.string("document_variants")).
           map(Document_Build.Document_Variant.parse)
 
       val dups = Library.duplicates(variants.map(_.name))
@@ -1403,8 +1408,11 @@
     def find_heap(name: String): Option[Path] =
       input_dirs.map(_ + heap(name)).find(_.is_file)
 
-    def find_heap_digest(name: String): Option[String] =
-      find_heap(name).flatMap(ML_Heap.read_digest)
+    def find_heap_shasum(name: String): SHA1.Shasum =
+      (for {
+        path <- find_heap(name)
+        digest <- ML_Heap.read_digest(path)
+      } yield SHA1.shasum(digest, name)).getOrElse(SHA1.no_shasum)
 
     def the_heap(name: String): Path =
       find_heap(name) getOrElse
@@ -1557,9 +1565,9 @@
           stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.compress)
           stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.compress)
           stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.compress)
-          stmt.string(8) = build.sources
-          stmt.string(9) = cat_lines(build.input_heaps)
-          stmt.string(10) = build.output_heap getOrElse ""
+          stmt.string(8) = build.sources.toString
+          stmt.string(9) = build.input_heaps.toString
+          stmt.string(10) = build.output_heap.toString
           stmt.int(11) = build.return_code
           stmt.string(12) = build.uuid
           stmt.execute()
@@ -1600,9 +1608,9 @@
               catch { case _: SQLException => "" }
             Some(
               Build.Session_Info(
-                res.string(Session_Info.sources),
-                split_lines(res.string(Session_Info.input_heaps)),
-                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
+                SHA1.fake_shasum(res.string(Session_Info.sources)),
+                SHA1.fake_shasum(res.string(Session_Info.input_heaps)),
+                SHA1.fake_shasum(res.string(Session_Info.output_heap)),
                 res.int(Session_Info.return_code),
                 uuid))
           }
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Tools/build.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -18,9 +18,9 @@
   /* persistent build info */
 
   sealed case class Session_Info(
-    sources: String,
-    input_heaps: List[String],
-    output_heap: Option[String],
+    sources: SHA1.Shasum,
+    input_heaps: SHA1.Shasum,
+    output_heap: SHA1.Shasum,
     return_code: Int,
     uuid: String
   ) {
@@ -209,14 +209,6 @@
         augment_options = augment_options)
     val full_sessions_selection = full_sessions.imports_selection(selection)
 
-    def sources_stamp(deps: Sessions.Deps, session_name: String): String = {
-      val digests =
-        full_sessions(session_name).meta_digest ::
-        deps.session_sources(session_name) :::
-        deps.imported_sources(session_name)
-      SHA1.digest_set(digests).toString
-    }
-
     val build_deps = {
       val deps0 =
         Sessions.deps(full_sessions.selection(selection),
@@ -230,7 +222,7 @@
               case Some(db) =>
                 using(db)(store.read_build(_, name)) match {
                   case Some(build)
-                  if build.ok && build.sources == sources_stamp(deps0, name) => None
+                  if build.ok && build.sources == deps0.sources_shasum(name) => None
                   case _ => Some(name)
                 }
               case None => Some(name)
@@ -279,7 +271,7 @@
     // scheduler loop
     case class Result(
       current: Boolean,
-      heap_digest: Option[String],
+      output_heap: SHA1.Shasum,
       process: Option[Process_Result],
       info: Sessions.Info
     ) {
@@ -306,7 +298,7 @@
 
     @tailrec def loop(
       pending: Queue,
-      running: Map[String, (List[String], Build_Job)],
+      running: Map[String, (SHA1.Shasum, Build_Job)],
       results: Map[String, Result]
     ): Map[String, Result] = {
       def used_node(i: Int): Boolean =
@@ -323,7 +315,7 @@
           case Some((session_name, (input_heaps, job))) =>
             //{{{ finish job
 
-            val (process_result, heap_digest) = job.join
+            val (process_result, output_heap) = job.join
 
             val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
             val process_result_tail = {
@@ -354,7 +346,7 @@
                 build_log =
                   if (process_result.timeout) build_log.error("Timeout") else build_log,
                 build =
-                  Session_Info(sources_stamp(build_deps, session_name), input_heaps, heap_digest,
+                  Session_Info(build_deps.sources_shasum(session_name), input_heaps, output_heap,
                     process_result.rc, UUID.random().toString)))
 
             // messages
@@ -371,7 +363,7 @@
 
             loop(pending - session_name, running - session_name,
               results +
-                (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
+                (session_name -> Result(false, output_heap, Some(process_result_tail), job.info)))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job
@@ -380,32 +372,32 @@
                 val ancestor_results =
                   build_deps.sessions_structure.build_requirements(List(session_name)).
                     filterNot(_ == session_name).map(results(_))
-                val ancestor_heaps =
+                val input_heaps =
                   if (ancestor_results.isEmpty) {
-                    List(SHA1.digest(Path.explode("$POLYML_EXE")).toString)
+                    SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
                   }
-                  else ancestor_results.flatMap(_.heap_digest)
+                  else SHA1.flat_shasum(ancestor_results.map(_.output_heap))
 
                 val do_store =
                   build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
 
-                val (current, heap_digest) = {
+                val (current, output_heap) = {
                   store.try_open_database(session_name) match {
                     case Some(db) =>
                       using(db)(store.read_build(_, session_name)) match {
                         case Some(build) =>
-                          val heap_digest = store.find_heap_digest(session_name)
+                          val output_heap = store.find_heap_shasum(session_name)
                           val current =
                             !fresh_build &&
                             build.ok &&
-                            build.sources == sources_stamp(build_deps, session_name) &&
-                            build.input_heaps == ancestor_heaps &&
-                            build.output_heap == heap_digest &&
-                            !(do_store && heap_digest.isEmpty)
-                          (current, heap_digest)
-                        case None => (false, None)
+                            build.sources == build_deps.sources_shasum(session_name) &&
+                            build.input_heaps == input_heaps &&
+                            build.output_heap == output_heap &&
+                            !(do_store && output_heap.is_empty)
+                          (current, output_heap)
+                        case None => (false, SHA1.no_shasum)
                       }
-                    case None => (false, None)
+                    case None => (false, SHA1.no_shasum)
                   }
                 }
                 val all_current = current && ancestor_results.forall(_.current)
@@ -413,13 +405,13 @@
                 if (all_current) {
                   loop(pending - session_name, running,
                     results +
-                      (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
+                      (session_name -> Result(true, output_heap, Some(Process_Result(0)), info)))
                 }
                 else if (no_build) {
                   progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
                     results +
-                      (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
+                      (session_name -> Result(false, output_heap, Some(Process_Result(1)), info)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
@@ -432,12 +424,12 @@
                   val job =
                     new Build_Job(progress, build_deps.background(session_name), store, do_store,
                       log, session_setup, numa_node, queue.command_timings(session_name))
-                  loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
+                  loop(pending, running + (session_name -> (input_heaps, job)), results)
                 }
                 else {
                   progress.echo(session_name + " CANCELLED")
                   loop(pending - session_name, running,
-                    results + (session_name -> Result(false, heap_digest, None, info)))
+                    results + (session_name -> Result(false, output_heap, None, info)))
                 }
               case None => sleep(); loop(pending, running, results)
             }
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Tools/build_job.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -570,7 +570,7 @@
     else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
   }
 
-  def join: (Process_Result, Option[String]) = {
+  def join: (Process_Result, SHA1.Shasum) = {
     val result1 = future_result.join
 
     val was_timeout =
@@ -585,12 +585,12 @@
       else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt"))
       else result1
 
-    val heap_digest =
+    val heap_shasum =
       if (result2.ok && do_store && store.output_heap(session_name).is_file) {
-        Some(ML_Heap.write_digest(store.output_heap(session_name)))
+        SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name)
       }
-      else None
+      else SHA1.no_shasum
 
-    (result2, heap_digest)
+    (result2, heap_shasum)
   }
 }
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Tools/dotnet_setup.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -186,7 +186,7 @@
           "V:" -> (arg => version = arg),
           "f" -> (_ => force = true),
           "n" -> (_ => dry_run = true),
-          "p:" -> (arg => platforms = Library.space_explode(',', arg).map(check_platform_spec)),
+          "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec)),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Tools/Setup/src/Build.java
--- a/src/Tools/Setup/src/Build.java	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Tools/Setup/src/Build.java	Mon Feb 06 21:32:22 2023 +0100
@@ -74,6 +74,7 @@
 
     public static String BUILD_PROPS = "build.props";
     public static String COMPONENT_BUILD_PROPS = "etc/build.props";
+    public static String META_INFO = "<meta_info>";
 
     public static String TITLE = "title";
     public static String MODULE = "module";
@@ -223,14 +224,14 @@
             return shasum(file, List.of(path(file)));
         }
 
-        public String shasum_props()
+        public String shasum_meta_info()
             throws NoSuchAlgorithmException, IOException, InterruptedException
         {
             TreeMap<String,Object> sorted = new TreeMap<String,Object>();
             for (Object x : _props.entrySet()) {
                 sorted.put(x.toString(), _props.get(x));
             }
-            return make_shasum("<props>",
+            return make_shasum(META_INFO,
                     sha -> sha.update(sorted.toString().getBytes(StandardCharsets.UTF_8)));
         }
     }
@@ -475,7 +476,7 @@
                 List<Path> compiler_deps = new LinkedList<Path>();
                 {
                     StringBuilder _shasum = new StringBuilder();
-                    _shasum.append(context.shasum_props());
+                    _shasum.append(context.shasum_meta_info());
                     for (String s : requirements) {
                         List<Path> paths = context.requirement_paths(s);
                         compiler_deps.addAll(paths);
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Tools/VSCode/src/build_vscode_extension.scala
--- a/src/Tools/VSCode/src/build_vscode_extension.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala	Mon Feb 06 21:32:22 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 8f2e6186408f -r 35a05e61c7b4 src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -426,7 +426,7 @@
   for targeting Windows.
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)),
-          "p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)),
+          "p:" -> (arg => platforms = space_explode(',', arg).map(Platform.Family.parse)),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Tools/VSCode/src/vscode_main.scala	Mon Feb 06 21:32:22 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] = {
diff -r 8f2e6186408f -r 35a05e61c7b4 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Feb 06 21:32:22 2023 +0100
@@ -107,7 +107,7 @@
     else if (path.is_basic && !prefix.endsWith("/") && !prefix.endsWith(JFile.separator))
       prefix + JFile.separator + File.platform_path(path)
     else if (path.is_basic) prefix + File.platform_path(path)
-    else File.absolute_name(new JFile(prefix + JFile.separator + File.platform_path(path)))
+    else File.absolute(new JFile(prefix + JFile.separator + File.platform_path(path))).getPath
   }
 
   override def read_dir(dir: String): List[String] =