tuned comments;
authorwenzelm
Mon, 27 Mar 2023 11:52:10 +0200
changeset 77720 f750047e9386
parent 77719 cbfbf48b0281
child 77721 7c1cc9ce9340
tuned comments;
src/Pure/ML/ml_heap.scala
src/Pure/Thy/sessions.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 */
+
 }
--- 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 =>