src/Pure/ML/ml_heap.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_heap.scala	Sun Jan 15 20:20:59 2023 +0100
@@ -0,0 +1,58 @@
+/*  Title:      Pure/ML/ml_heap.scala
+    Author:     Makarius
+
+ML heap operations.
+*/
+
+package isabelle
+
+
+import java.nio.ByteBuffer
+import java.nio.channels.FileChannel
+import java.nio.file.StandardOpenOption
+
+
+object ML_Heap {
+  /** heap file with SHA1 digest **/
+
+  private val sha1_prefix = "SHA1:"
+
+  def read_digest(heap: Path): Option[String] = {
+    if (heap.is_file) {
+      using(FileChannel.open(heap.java_path, StandardOpenOption.READ)) { file =>
+        val len = file.size
+        val n = sha1_prefix.length + SHA1.digest_length
+        if (len >= n) {
+          file.position(len - n)
+
+          val buf = ByteBuffer.allocate(n)
+          var i = 0
+          var m = 0
+          while ({
+            m = file.read(buf)
+            if (m != -1) i += m
+            m != -1 && n > i
+          }) ()
+
+          if (i == n) {
+            val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
+            val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
+            if (prefix == sha1_prefix) Some(s) else None
+          }
+          else None
+        }
+        else None
+      }
+    }
+    else None
+  }
+
+  def write_digest(heap: Path): String =
+    read_digest(heap) match {
+      case None =>
+        val s = SHA1.digest(heap).toString
+        File.append(heap, sha1_prefix + s)
+        s
+      case Some(s) => s
+    }
+}