store session sources within build database: timing e.g. 150ms for HOL and < 50ms for common sessions;
enforce rebuild of Isabelle/ML to update build databases;

--- a/src/Pure/ROOT.ML	Sat Dec 31 15:48:12 2022 +0100
+++ b/src/Pure/ROOT.ML	Sun Jan 01 21:44:08 2023 +0100
@@ -366,4 +366,3 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML";
-

--- a/src/Pure/Thy/export.scala	Sat Dec 31 15:48:12 2022 +0100
+++ b/src/Pure/Thy/export.scala	Sun Jan 01 21:44:08 2023 +0100
@@ -423,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

--- a/src/Pure/Thy/sessions.scala	Sat Dec 31 15:48:12 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Jan 01 21:44:08 2023 +0100
@@ -1337,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)
 
@@ -1495,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())
@@ -1521,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)
@@ -1588,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)
+        }
+      }
+    }
   }
 }

--- a/src/Pure/Tools/build.scala	Sat Dec 31 15:48:12 2022 +0100
+++ b/src/Pure/Tools/build.scala	Sun Jan 01 21:44:08 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 =