# HG changeset patch
# User wenzelm
# Date 1679910730 -7200
# Node ID f750047e93861fba501f34e4ab7f327e57925bfc
# Parent  cbfbf48b0281a28f9285719ed996562b60e7bf20
tuned comments;

diff -r cbfbf48b0281 -r f750047e9386 src/Pure/ML/ml_heap.scala
--- 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 */
+
 }
diff -r cbfbf48b0281 -r f750047e9386 src/Pure/Thy/sessions.scala
--- 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 =>