proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;

--- a/src/Pure/General/file.scala	Thu Mar 24 13:22:02 2016 +0100
+++ b/src/Pure/General/file.scala	Thu Mar 24 14:55:43 2016 +0100
@@ -264,14 +264,4 @@
   }
 
   def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
-
-
-  /* approximative time stamp */
-
-  def time_stamp(path: Path): Option[String] =
-  {
-    val file = path.file
-    if (file.isFile) Some(file.length.toString + " " + file.lastModified.toString)
-    else None
-  }
 }

--- a/src/Pure/General/sha1.scala	Thu Mar 24 13:22:02 2016 +0100
+++ b/src/Pure/General/sha1.scala	Thu Mar 24 14:55:43 2016 +0100
@@ -56,6 +56,8 @@
     make_result(digest)
   }
 
+  def digest(path: Path): Digest = digest(path.file)
+
   def digest(bytes: Array[Byte]): Digest =
   {
     val digest = MessageDigest.getInstance("SHA")

--- a/src/Pure/Thy/sessions.scala	Thu Mar 24 13:22:02 2016 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 24 14:55:43 2016 +0100
@@ -6,6 +6,9 @@
 
 package isabelle
 
+import java.nio.ByteBuffer
+import java.nio.channels.FileChannel
+import java.nio.file.StandardOpenOption
 
 import scala.collection.SortedSet
 import scala.collection.mutable
@@ -319,6 +322,54 @@
 
 
 
+  /** heap file with SHA1 digest **/
+
+  private val sha1_prefix = "SHA1:"
+
+  def read_heap_digest(heap: Path): Option[String] =
+  {
+    if (heap.is_file) {
+      val file = FileChannel.open(heap.file.toPath, StandardOpenOption.READ)
+      try {
+        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
+          do {
+            m = file.read(buf)
+            if (m != -1) i += m
+          }
+          while (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
+      }
+      finally { file.close }
+    }
+    else None
+  }
+
+  def write_heap_digest(heap: Path): String =
+    read_heap_digest(heap) match {
+      case None =>
+        val s = SHA1.digest(heap).rep
+        File.append(heap, sha1_prefix + s)
+        s
+      case Some(s) => s
+    }
+
+
+
   /** persistent store **/
 
   def log(name: String): Path = Path.basic("log") + Path.basic(name)
@@ -352,7 +403,7 @@
 
     def find(name: String): Option[(Path, Option[String])] =
       input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
-        (dir + log_gz(name), File.time_stamp(dir + Path.basic(name))))
+        (dir + log_gz(name), read_heap_digest(dir + Path.basic(name))))
 
     def find_log(name: String): Option[Path] =
       input_dirs.map(_ + log(name)).find(_.is_file)

--- a/src/Pure/Tools/build.scala	Thu Mar 24 13:22:02 2016 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 24 14:55:43 2016 +0100
@@ -560,8 +560,8 @@
               if (process_result.ok) {
                 (store.output_dir + Sessions.log(name)).file.delete
                 val heap_stamp =
-                  for (path <- job.output_path; stamp <- File.time_stamp(path))
-                    yield stamp
+                  for (path <- job.output_path if path.is_file)
+                    yield Sessions.write_heap_digest(path)
 
                 File.write_gzip(store.output_dir + Sessions.log_gz(name),
                   Library.terminate_lines(