# HG changeset patch
# User wenzelm
# Date 1672606913 -3600
# Node ID 3bd08d0432d72129b66adc10891aa5664718424b
# Parent  04c7ec38874e8a8805cb690dcf3b3e9de8f70c88# Parent  90c552d28d360c1888d77ffeab956fb858ee746e
merged

diff -r 04c7ec38874e -r 3bd08d0432d7 etc/build.props
--- a/etc/build.props	Sun Jan 01 12:24:00 2023 +0000
+++ b/etc/build.props	Sun Jan 01 22:01:53 2023 +0100
@@ -315,7 +315,7 @@
   isabelle.Scala$Handler \
   isabelle.Scala_Functions \
   isabelle.Server_Commands \
-  isabelle.Sessions$File_Format \
+  isabelle.Sessions$ROOTS_File_Format \
   isabelle.Simplifier_Trace$Handler \
   isabelle.Tools \
   isabelle.jedit.JEdit_Plugin0 \
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/General/graph.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -27,7 +27,7 @@
 
   def make[Key, A](
     entries: List[((Key, A), List[Key])],
-    symmetric: Boolean = false)(
+    converse: Boolean = false)(
     implicit ord: Ordering[Key]
   ): Graph[Key, A] = {
     val graph1 =
@@ -38,7 +38,7 @@
       entries.foldLeft(graph1) {
         case (graph, ((x, _), ys)) =>
           ys.foldLeft(graph) {
-            case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y)
+            case (g, y) => if (converse) g.add_edge(y, x) else g.add_edge(x, y)
           }
       }
     graph2
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/General/url.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -102,7 +102,7 @@
   def canonical_file_name(uri: String): String = canonical_file(uri).getPath
 
 
-  /* generic path notation: local, ssh, rsync, ftp, http */
+  /* generic path notation: standard, platform, ssh, rsync, ftp, http */
 
   private val separators1 = "/\\"
   private val separators2 = ":/\\"
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/PIDE/document.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -94,6 +94,9 @@
       def apply(node: String, master_dir: String = "", theory: String = ""): Name =
         new Name(node, master_dir, theory)
 
+      def loaded_theory(theory: String): Document.Node.Name =
+        Name(theory, theory = theory)
+
       val empty: Name = Name("")
 
       object Ordering extends scala.math.Ordering[Name] {
@@ -103,7 +106,7 @@
       type Graph[A] = isabelle.Graph[Node.Name, A]
 
       def make_graph[A](entries: List[((Name, A), List[Name])]): Graph[A] =
-        Graph.make(entries, symmetric = true)(Ordering)
+        Graph.make(entries, converse = true)(Ordering)
     }
 
     final class Name private(val node: String, val master_dir: String, val theory: String) {
@@ -125,16 +128,11 @@
 
       override def toString: String = if (is_theory) theory else node
 
-      def map(f: String => String): Name =
-        new Name(f(node), f(master_dir), theory)
-
       def json: JSON.Object.T =
         JSON.Object("node_name" -> node, "theory_name" -> theory)
     }
 
     sealed case class Entry(name: Node.Name, header: Node.Header) {
-      def map(f: String => String): Entry = copy(name = name.map(f))
-
       override def toString: String = name.toString
     }
 
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/PIDE/protocol.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -28,7 +28,7 @@
         case (Markup.Name(name), Position.File(file), Position.Id(id))
         if Path.is_wellformed(file) =>
           val master_dir = Path.explode(file).dir.implode
-          Some((Document.Node.Name(file, master_dir, name), id))
+          Some((Document.Node.Name(file, master_dir = master_dir, theory = name), id))
         case _ => None
       }
   }
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/PIDE/resources.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -78,12 +78,9 @@
   def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = {
     val node = append(dir, file)
     val master_dir = append(dir, file.dir)
-    Document.Node.Name(node, master_dir, theory)
+    Document.Node.Name(node, master_dir = master_dir, theory = theory)
   }
 
-  def loaded_theory_node(theory: String): Document.Node.Name =
-    Document.Node.Name(theory, "", theory)
-
 
   /* source files of Isabelle/ML bootstrap */
 
@@ -141,7 +138,7 @@
     for {
       (name, theory) <- Thy_Header.ml_roots
       path = (pure_dir + Path.explode(name)).expand
-      node_name = Document.Node.Name(path.implode, path.dir.implode, theory)
+      node_name = Document.Node.Name(path.implode, master_dir = path.dir.implode, theory = theory)
       file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)())
     } yield file
   }
@@ -175,12 +172,12 @@
     if (literal_import && !Url.is_base_name(s)) {
       error("Bad import of theory from other session via file-path: " + quote(s))
     }
-    if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+    if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
     else {
       find_theory_node(theory) match {
         case Some(node_name) => node_name
         case None =>
-          if (Url.is_base_name(s) && literal_theory(s)) loaded_theory_node(theory)
+          if (Url.is_base_name(s) && literal_theory(s)) Document.Node.Name.loaded_theory(theory)
           else file_node(Path.explode(s).thy, dir = dir, theory = theory)
       }
     }
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/PIDE/session.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -487,7 +487,7 @@
               case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
                 val id = Value.Long.unapply(args.id.get).get
-                val entry = Export.make_entry(Sessions.DRAFT, args, msg.chunk, cache)
+                val entry = Export.Entry.make(Sessions.DRAFT, args, msg.chunk, cache)
                 change_command(_.add_export(id, (args.serial, entry)))
 
               case Protocol.Loading_Theory(node_name, id) =>
@@ -563,7 +563,7 @@
                 val snapshot = global_state.change_result(_.end_theory(id))
                 finished_theories.post(snapshot)
               }
-              file_formats.stop_session
+              file_formats.stop_session()
               phase = Session.Terminated(result)
               prover.reset()
 
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/ROOT.ML	Sun Jan 01 22:01:53 2023 +0100
@@ -366,4 +366,3 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML";
-
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/bibtex.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -28,6 +28,7 @@
     override def theory_content(name: String): String =
       """theory "bib" imports Pure begin bibtex_file """ +
         Outer_Syntax.quote_string(name) + """ end"""
+    override def theory_excluded(name: String): Boolean = name == "bib"
 
     override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = {
       val name = snapshot.node_name
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/export.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -107,13 +107,36 @@
   def message(msg: String, theory_name: String, name: String): String =
     msg + " " + quote(name) + " for theory " + quote(theory_name)
 
-  def empty_entry(theory_name: String, name: String): Entry =
-    Entry(Entry_Name(theory = theory_name, name = name),
-      false, Future.value(false, Bytes.empty), XML.Cache.none)
+  object Entry {
+    def apply(
+      entry_name: Entry_Name,
+      executable: Boolean,
+      body: Future[(Boolean, Bytes)],
+      cache: XML.Cache
+    ): Entry = new Entry(entry_name, executable, body, cache)
+
+    def empty(theory_name: String, name: String): Entry =
+      Entry(Entry_Name(theory = theory_name, name = name),
+        false, Future.value(false, Bytes.empty), XML.Cache.none)
 
-  sealed case class Entry(
-    entry_name: Entry_Name,
-    executable: Boolean,
+    def make(
+      session_name: String,
+      args: Protocol.Export.Args,
+      bytes: Bytes,
+      cache: XML.Cache
+    ): Entry = {
+      val body =
+        if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.compress))
+        else Future.value((false, bytes))
+      val entry_name =
+        Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
+      Entry(entry_name, args.executable, body, cache)
+    }
+  }
+
+  final class Entry private(
+    val entry_name: Entry_Name,
+    val executable: Boolean,
     body: Future[(Boolean, Bytes)],
     cache: XML.Cache
   ) {
@@ -122,6 +145,9 @@
     def name: String = entry_name.name
     override def toString: String = name
 
+    def is_finished: Boolean = body.is_finished
+    def cancel(): Unit = body.cancel()
+
     def compound_name: String = entry_name.compound_name
 
     def name_has_prefix(s: String): Boolean = name.startsWith(s)
@@ -130,25 +156,24 @@
     def name_extends(elems: List[String]): Boolean =
       name_elems.startsWith(elems) && name_elems != elems
 
-    def text: String = uncompressed.text
-
-    def uncompressed: Bytes = {
-      val (compressed, bytes) = body.join
-      if (compressed) bytes.uncompress(cache = cache.compress) else bytes
+    def bytes: Bytes = {
+      val (compressed, bs) = body.join
+      if (compressed) bs.uncompress(cache = cache.compress) else bs
     }
 
-    def uncompressed_yxml: XML.Body =
-      YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache)
+    def text: String = bytes.text
+
+    def yxml: XML.Body = YXML.parse_body(UTF8.decode_permissive(bytes), cache = cache)
 
     def write(db: SQL.Database): Unit = {
-      val (compressed, bytes) = body.join
+      val (compressed, bs) = body.join
       db.using_statement(Data.table.insert()) { stmt =>
         stmt.string(1) = session_name
         stmt.string(2) = theory_name
         stmt.string(3) = name
         stmt.bool(4) = executable
         stmt.bool(5) = compressed
-        stmt.bytes(6) = bytes
+        stmt.bytes(6) = bs
         stmt.execute()
       }
     }
@@ -176,19 +201,6 @@
     (entry_name: Entry_Name) => regs.exists(_.matches(entry_name.compound_name))
   }
 
-  def make_entry(
-    session_name: String,
-    args: Protocol.Export.Args,
-    bytes: Bytes,
-    cache: XML.Cache
-  ): Entry = {
-    val body =
-      if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.compress))
-      else Future.value((false, bytes))
-    val entry_name = Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
-    Entry(entry_name, args.executable, body, cache)
-  }
-
 
   /* database consumer thread */
 
@@ -200,7 +212,7 @@
 
     private val consumer =
       Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
-        bulk = { case (entry, _) => entry.body.is_finished },
+        bulk = { case (entry, _) => entry.is_finished },
         consume =
           { (args: List[(Entry, Boolean)]) =>
             val results =
@@ -208,7 +220,7 @@
                 for ((entry, strict) <- args)
                 yield {
                   if (progress.stopped) {
-                    entry.body.cancel()
+                    entry.cancel()
                     Exn.Res(())
                   }
                   else if (entry.entry_name.readable(db)) {
@@ -227,7 +239,7 @@
     def make_entry(session_name: String, args0: Protocol.Export.Args, body: Bytes): Unit = {
       if (!progress.stopped && !body.is_empty) {
         val args = if (db.is_server) args0.copy(compress = false) else args0
-        consumer.send(Export.make_entry(session_name, args, body, cache) -> args.strict)
+        consumer.send(Entry.make(session_name, args, body, cache) -> args.strict)
       }
     }
 
@@ -403,7 +415,7 @@
 
     def apply(theory: String, name: String, permissive: Boolean = false): Entry =
       get(theory, name) match {
-        case None if permissive => empty_entry(theory, name)
+        case None if permissive => Entry.empty(theory, name)
         case None => error("Missing export entry " + quote(compound_name(theory, name)))
         case Some(entry) => entry
       }
@@ -411,6 +423,20 @@
     def theory(theory: String, other_cache: Option[Term.Cache] = None): Theory_Context =
       new Theory_Context(session_context, theory, other_cache)
 
+    def node_source(name: Document.Node.Name): String = {
+      def snapshot_source: Option[String] =
+        for {
+          snapshot <- document_snapshot
+          node = snapshot.get_node(name)
+          text = node.source if text.nonEmpty
+        } yield text
+      def db_source: Option[String] =
+        db_hierarchy.view.map(database =>
+            database_context.store.read_sources(database.db, database.session, name.node))
+          .collectFirst({ case Some(bytes) => bytes.text })
+      snapshot_source orElse db_source getOrElse ""
+    }
+
     def classpath(): List[File.Content] = {
       (for {
         session <- session_stack.iterator
@@ -420,7 +446,7 @@
         entry_name <- entry_names(session = session).iterator
         if matcher(entry_name)
         entry <- get(entry_name.theory, entry_name.name).iterator
-      } yield File.content(entry.entry_name.make_path(), entry.uncompressed)).toList
+      } yield File.content(entry.entry_name.make_path(), entry.bytes)).toList
     }
 
     override def toString: String =
@@ -438,9 +464,9 @@
     def apply(name: String, permissive: Boolean = false): Entry =
       session_context.apply(theory, name, permissive = permissive)
 
-    def uncompressed_yxml(name: String): XML.Body =
+    def yxml(name: String): XML.Body =
       get(name) match {
-        case Some(entry) => entry.uncompressed_yxml
+        case Some(entry) => entry.yxml
         case None => Nil
       }
 
@@ -492,7 +518,7 @@
           val path = export_dir + entry_name.make_path(prune = export_prune)
           progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
           Isabelle_System.make_directory(path.dir)
-          val bytes = entry.uncompressed
+          val bytes = entry.bytes
           if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
           File.set_executable(path, entry.executable)
         }
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/export_theory.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -103,7 +103,7 @@
 
   def read_theory_parents(theory_context: Export.Theory_Context): Option[List[String]] =
     theory_context.get(Export.THEORY_PREFIX + "parents")
-      .map(entry => Library.trim_split_lines(entry.uncompressed.text))
+      .map(entry => Library.trim_split_lines(entry.text))
 
   def theory_names(
     session_context: Export.Session_Context,
@@ -233,7 +233,7 @@
         case _ => err()
       }
     }
-    theory_context.uncompressed_yxml(export_name).map(decode_entity)
+    theory_context.yxml(export_name).map(decode_entity)
   }
 
 
@@ -393,7 +393,7 @@
 
     for { entry <- theory_context.get(Export.PROOFS_PREFIX + id.serial) }
     yield {
-      val body = entry.uncompressed_yxml
+      val body = entry.yxml
       val (typargs, (args, (prop_body, proof_body))) = {
         import XML.Decode._
         import Term_XML.Decode._
@@ -539,7 +539,7 @@
   }
 
   def read_classrel(theory_context: Export.Theory_Context): List[Classrel] = {
-    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "classrel")
+    val body = theory_context.yxml(Export.THEORY_PREFIX + "classrel")
     val classrel = {
       import XML.Decode._
       list(pair(decode_prop, pair(string, string)))(body)
@@ -559,7 +559,7 @@
   }
 
   def read_arities(theory_context: Export.Theory_Context): List[Arity] = {
-    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "arities")
+    val body = theory_context.yxml(Export.THEORY_PREFIX + "arities")
     val arities = {
       import XML.Decode._
       import Term_XML.Decode._
@@ -577,7 +577,7 @@
   }
 
   def read_constdefs(theory_context: Export.Theory_Context): List[Constdef] = {
-    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs")
+    val body = theory_context.yxml(Export.THEORY_PREFIX + "constdefs")
     val constdefs = {
       import XML.Decode._
       list(pair(string, string))(body)
@@ -606,7 +606,7 @@
   }
 
   def read_typedefs(theory_context: Export.Theory_Context): List[Typedef] = {
-    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs")
+    val body = theory_context.yxml(Export.THEORY_PREFIX + "typedefs")
     val typedefs = {
       import XML.Decode._
       import Term_XML.Decode._
@@ -640,7 +640,7 @@
   }
 
   def read_datatypes(theory_context: Export.Theory_Context): List[Datatype] = {
-    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes")
+    val body = theory_context.yxml(Export.THEORY_PREFIX + "datatypes")
     val datatypes = {
       import XML.Decode._
       import Term_XML.Decode._
@@ -730,7 +730,7 @@
   }
 
   def read_spec_rules(theory_context: Export.Theory_Context): List[Spec_Rule] = {
-    val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules")
+    val body = theory_context.yxml(Export.THEORY_PREFIX + "spec_rules")
     val spec_rules = {
       import XML.Decode._
       import Term_XML.Decode._
@@ -753,7 +753,7 @@
   def read_others(theory_context: Export.Theory_Context): Map[String, List[Entity[Other]]] = {
     val kinds =
       theory_context.get(Export.THEORY_PREFIX + "other_kinds") match {
-        case Some(entry) => split_lines(entry.uncompressed.text)
+        case Some(entry) => split_lines(entry.text)
         case None => Nil
       }
     val other = Other()
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/file_format.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -28,6 +28,8 @@
     def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
     def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined
 
+    def theory_excluded(name: String): Boolean = file_formats.exists(_.theory_excluded(name))
+
     def parse_data(name: String, text: String): AnyRef =
       get(name) match {
         case Some(file_format) => file_format.parse_data(name, text)
@@ -49,7 +51,7 @@
     def prover_options(options: Options): Options =
       agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) }
 
-    def stop_session: Unit = agents.foreach(_.stop())
+    def stop_session(): Unit = agents.foreach(_.stop())
   }
 
   trait Agent {
@@ -74,18 +76,19 @@
 
   def theory_suffix: String = ""
   def theory_content(name: String): String = ""
+  def theory_excluded(name: String): Boolean = false
 
   def make_theory_name(
     resources: Resources,
     name: Document.Node.Name
   ): Option[Document.Node.Name] = {
     for {
-      thy <- Url.get_base_name(name.node)
+      theory <- Url.get_base_name(name.node)
       if detect(name.node) && theory_suffix.nonEmpty
     }
     yield {
-      val thy_node = resources.append(name.node, Path.explode(theory_suffix))
-      Document.Node.Name(thy_node, name.master_dir, thy)
+      val node = resources.append(name.node, Path.explode(theory_suffix))
+      Document.Node.Name(node, master_dir = name.master_dir, theory = theory)
     }
   }
 
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/sessions.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -32,12 +32,13 @@
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
   def illegal_session(name: String): Boolean = name == "" || name == DRAFT
-  def illegal_theory(name: String): Boolean = name == root_name || name == "bib"
+  def illegal_theory(name: String): Boolean =
+    name == root_name || File_Format.registry.theory_excluded(name)
 
 
   /* ROOTS file format */
 
-  class File_Format extends isabelle.File_Format {
+  class ROOTS_File_Format extends File_Format {
     val format_name: String = roots_name
     val file_ext = ""
 
@@ -51,6 +52,7 @@
     override def theory_content(name: String): String =
       """theory "ROOTS" imports Pure begin ROOTS_file """ +
         Outer_Syntax.quote_string(name) + """ end"""
+    override def theory_excluded(name: String): Boolean = name == "ROOTS"
   }
 
 
@@ -247,7 +249,7 @@
     var cache_sources = Map.empty[JFile, SHA1.Digest]
     def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = {
       for {
-        path <- paths
+        path <- Library.distinct(paths)
         file = path.file
         if cache_sources.isDefinedAt(file) || file.isFile
       }
@@ -1335,6 +1337,21 @@
       " ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql)
   }
 
+  object Sources {
+    val session_name = SQL.Column.string("session_name").make_primary_key
+    val name = SQL.Column.string("name").make_primary_key
+    val digest = SQL.Column.string("digest")
+    val compressed = SQL.Column.bool("compressed")
+    val body = SQL.Column.bytes("body")
+
+    val table =
+      SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body))
+
+    def where_equal(session_name: String, name: String = ""): SQL.Source =
+      "WHERE " + Sources.session_name.equal(session_name) +
+        (if (name == "") "" else " AND " + Sources.name.equal(name))
+  }
+
   def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
     new Store(options, cache)
 
@@ -1493,6 +1510,9 @@
           db.using_statement(Session_Info.augment_table)(_.execute())
         }
 
+        db.create_table(Sources.table)
+        db.using_statement(Sources.table.delete(Sources.where_equal(name)))(_.execute())
+
         db.create_table(Export.Data.table)
         db.using_statement(
           Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute())
@@ -1519,14 +1539,33 @@
 
     def write_session_info(
       db: SQL.Database,
-      name: String,
+      session_base: Base,
       build_log: Build_Log.Session_Info,
       build: Build.Session_Info
     ): Unit = {
+      val sources =
+        for ((path, digest) <- session_base.session_sources) yield {
+          val bytes = Bytes.read(path)
+          if (bytes.sha1_digest != digest) error("Erratic change of file content: " + path)
+          val name = path.implode_symbolic
+          val (compressed, body) =
+            bytes.maybe_compress(Compress.Options_Zstd(), cache = cache.compress)
+          (name, digest, compressed, body)
+        }
+
       db.transaction {
-        val table = Session_Info.table
-        db.using_statement(table.insert()) { stmt =>
-          stmt.string(1) = name
+        for ((name, digest, compressed, body) <- sources) {
+          db.using_statement(Sources.table.insert()) { stmt =>
+            stmt.string(1) = session_base.session_name
+            stmt.string(2) = name
+            stmt.string(3) = digest.toString
+            stmt.bool(4) = compressed
+            stmt.bytes(5) = body
+            stmt.execute()
+          }
+        }
+        db.using_statement(Session_Info.table.insert()) { stmt =>
+          stmt.string(1) = session_base.session_name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
           stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.compress)
           stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.compress)
@@ -1586,5 +1625,20 @@
       }
       else None
     }
+
+    def read_sources(db: SQL.Database, session_name: String, name: String): Option[Bytes] = {
+      val sql =
+        Sources.table.select(List(Sources.compressed, Sources.body),
+          Sources.where_equal(session_name, name = name))
+      db.using_statement(sql) { stmt =>
+        val res = stmt.execute_query()
+        if (!res.next()) None
+        else {
+          val compressed = res.bool(Sources.compressed)
+          val bs = res.bytes(Sources.body)
+          Some(if (compressed) bs.uncompress(cache = cache.compress) else bs)
+        }
+      }
+    }
   }
 }
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/thy_header.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -93,7 +93,8 @@
 
   def theory_name(s: String): String =
     get_thy_name(s) match {
-      case Some(name) => bootstrap_name(name)
+      case Some(name) =>
+        bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
       case None =>
         Url.get_base_name(s) match {
           case Some(name) =>
@@ -109,9 +110,6 @@
   def is_bootstrap(theory: String): Boolean =
     bootstrap_thys.exists({ case (_, b) => b == theory })
 
-  def bootstrap_name(theory: String): String =
-    bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
-
 
   /* parser */
 
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Tools/build.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -348,7 +348,7 @@
 
             // write database
             using(store.open_database(session_name, output = true))(db =>
-              store.write_session_info(db, session_name,
+              store.write_session_info(db, build_deps(session_name),
                 build_log =
                   if (process_result.timeout) build_log.error("Timeout") else build_log,
                 build =
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Tools/build_job.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -22,7 +22,7 @@
 
     def read_xml(name: String): XML.Body =
       YXML.parse_body(
-        Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)),
+        Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).bytes)),
         cache = theory_context.cache)
 
     for {
@@ -274,8 +274,8 @@
           override val cache: Term.Cache = store.cache
 
           override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = {
-            val name1 = name.map(s => Path.explode(s).expand.implode)
-            session_background.base.load_commands.get(name1) match {
+            val expand_node = Document.Node.Name(Path.explode(name.node).expand.implode)
+            session_background.base.load_commands.get(expand_node) match {
               case Some(spans) =>
                 val syntax = session_background.base.theory_syntax(name)
                 Command.build_blobs_info(syntax, name, spans)
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Tools/dump.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -57,13 +57,13 @@
           for {
             entry <- args.snapshot.exports
             if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
-          } args.write(Path.explode(entry.name), entry.uncompressed)),
+          } args.write(Path.explode(entry.name), entry.bytes)),
       Aspect("theory", "foundational theory content",
         args =>
           for {
             entry <- args.snapshot.exports
             if entry.name_has_prefix(Export.THEORY_PREFIX)
-          } args.write(Path.explode(entry.name), entry.uncompressed),
+          } args.write(Path.explode(entry.name), entry.bytes),
         options = List("export_theory"))
     ).sortBy(_.name)
 
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Tools/server_commands.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -266,7 +266,7 @@
                     val matcher = Export.make_matcher(List(args.export_pattern))
                     for { entry <- snapshot.exports if matcher(entry.entry_name) }
                     yield {
-                      val (base64, body) = entry.uncompressed.maybe_encode_base64
+                      val (base64, body) = entry.bytes.maybe_encode_base64
                       JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
                     }
                   }))
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -93,10 +93,10 @@
     find_theory(file) getOrElse {
       val node = file.getPath
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
-      if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
       else {
         val master_dir = file.getParent
-        Document.Node.Name(node, master_dir, theory)
+        Document.Node.Name(node, master_dir = master_dir, theory = theory)
       }
     }
 
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Tools/jEdit/src/isabelle_export.scala
--- a/src/Tools/jEdit/src/isabelle_export.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Tools/jEdit/src/isabelle_export.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -56,7 +56,7 @@
                 } yield {
                   val is_dir = entry.name_elems.length > depth
                   val path = Export.implode_name(theory :: entry.name_elems.take(depth))
-                  val file_size = if (is_dir) None else Some(entry.uncompressed.length.toLong)
+                  val file_size = if (is_dir) None else Some(entry.bytes.length.toLong)
                   (path, file_size)
                 }).toSet.toList
               (for ((path, file_size) <- entries.iterator) yield {
@@ -86,7 +86,7 @@
               if node_name.theory == theory
               (_, entry) <- snapshot.state.node_exports(version, node_name).iterator
               if entry.name_elems == name_elems
-            } yield entry.uncompressed).find(_ => true).getOrElse(Bytes.empty)
+            } yield entry.bytes).find(_ => true).getOrElse(Bytes.empty)
 
           bytes.stream()
       }
diff -r 04c7ec38874e -r 3bd08d0432d7 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 01 22:01:53 2023 +0100
@@ -35,10 +35,10 @@
       val vfs = VFSManager.getVFSForPath(path)
       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
-      if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
       else {
         val master_dir = vfs.getParentOfPath(path)
-        Document.Node.Name(node, master_dir, theory)
+        Document.Node.Name(node, master_dir = master_dir, theory = theory)
       }
     }