src/Pure/ML/ml_heap.scala

         body = "SELECT name, slice, pg_size_pretty(length(content)::bigint) as size FROM " +
           Slices.table.ident,
         name = "slices_size")
     }
 
-    def get_entries(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] = {
+    def read_digests(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] = {
       require(names.nonEmpty)
 
       db.execute_query_statement(
         Base.table.select(List(Base.name, Base.digest),
           sql = Generic.name.where_member(names)),

         case (_, "") => None
         case (name, digest) => Some(name -> SHA1.fake_digest(digest))
       }).toMap
     }
 
-    def read_entry(db: SQL.Database, name: String): List[Bytes] =
+    def read_slices(db: SQL.Database, name: String): List[Bytes] =
       db.execute_query_statement(
         Slices.table.select(List(Slices.content),
           sql = Generic.name.where_equal(name) + SQL.order_by(List(Slices.slice))),
         List.from[Bytes], _.bytes(Slices.content))
 

           stmt.string(1) = name
           stmt.long(2) = None
           stmt.string(3) = None
         })
 
-    def write_entry(db: SQL.Database, name: String, slice: Int, content: Bytes): Unit =
+    def write_slice(db: SQL.Database, name: String, slice: Int, content: Bytes): Unit =
       db.execute_statement(Slices.table.insert(), body =
       { stmt =>
         stmt.string(1) = name
         stmt.int(2) = slice
         stmt.bytes(3) = content

   def clean_entry(db: SQL.Database, session_name: String): Unit =
     private_data.transaction_lock(db, create = true, label = "ML_Heap.clean_entry") {
       private_data.clean_entry(db, session_name)
     }
 
-  def get_entries(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] =
-    private_data.transaction_lock(db, create = true, label = "ML_Heap.get_entries") {
-      private_data.get_entries(db, names)
+  def read_digests(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] =
+    private_data.transaction_lock(db, create = true, label = "ML_Heap.read_digests") {
+      private_data.read_digests(db, names)
     }
 
   def store(
     database: Option[SQL.Database],
     session_name: String,

             val limit = if (j < slices) step * j else size
             val content =
               Bytes.read_file(heap, offset = offset, limit = limit)
                 .compress(cache = cache)
             private_data.transaction_lock(db, label = "ML_Heap.store2") {
-              private_data.write_entry(db, session_name, i, content)
+              private_data.write_slice(db, session_name, i, content)
             }
           }
 
           private_data.transaction_lock(db, label = "ML_Heap.store3") {
             private_data.finish_entry(db, session_name, size, digest)

     cache: Compress.Cache = Compress.Cache.none
   ): Unit = {
     database match {
       case Some(db) if heaps.nonEmpty =>
         private_data.transaction_lock(db, create = true, label = "ML_Heap.restore") {
-          val db_digests = private_data.get_entries(db, heaps.map(_.file_name))
+          val db_digests = private_data.read_digests(db, heaps.map(_.file_name))
           for (heap <- heaps) {
             val session_name = heap.file_name
             val file_digest = read_file_digest(heap)
             val db_digest = db_digests.get(session_name)
             if (db_digest.isDefined && db_digest != file_digest) {
               val base_dir = Isabelle_System.make_directory(heap.expand.dir)
               Isabelle_System.with_tmp_file(session_name + "_", base_dir = base_dir.file) { tmp =>
                 Bytes.write(tmp, Bytes.empty)
-                for (slice <- private_data.read_entry(db, session_name)) {
+                for (slice <- private_data.read_slices(db, session_name)) {
                   Bytes.append(tmp, slice.uncompress(cache = cache))
                 }
                 val digest = write_file_digest(tmp)
                 if (db_digest.get == digest) {
                   Isabelle_System.chmod("a+r", tmp)