--- a/src/Pure/ML/ml_heap.scala Sun Mar 26 20:03:03 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala Mon Mar 27 11:52:10 2023 +0200
@@ -39,4 +39,8 @@
File.append(heap, sha1_prefix + digest.toString)
digest
}
+
+
+ /* SQL data model */
+
}
--- a/src/Pure/Thy/sessions.scala Sun Mar 26 20:03:03 2023 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Mar 27 11:52:10 2023 +0200
@@ -1392,7 +1392,7 @@
/** persistent store **/
- /** auxiliary **/
+ /* SQL data model */
sealed case class Build_Info(
sources: SHA1.Shasum,
@@ -1433,6 +1433,9 @@
" ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql)
}
+
+ /* store */
+
class Store private[Sessions](val options: Options, val cache: Term.Cache) {
store =>