src/Pure/Thy/sessions.scala
changeset 62704 478b49f0d726
parent 62637 0189fe0f6452
child 62769 146945b9e83c
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Mar 24 13:22:02 2016 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Mar 24 14:55:43 2016 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  package isabelle
     1.6  
     1.7 +import java.nio.ByteBuffer
     1.8 +import java.nio.channels.FileChannel
     1.9 +import java.nio.file.StandardOpenOption
    1.10  
    1.11  import scala.collection.SortedSet
    1.12  import scala.collection.mutable
    1.13 @@ -319,6 +322,54 @@
    1.14  
    1.15  
    1.16  
    1.17 +  /** heap file with SHA1 digest **/
    1.18 +
    1.19 +  private val sha1_prefix = "SHA1:"
    1.20 +
    1.21 +  def read_heap_digest(heap: Path): Option[String] =
    1.22 +  {
    1.23 +    if (heap.is_file) {
    1.24 +      val file = FileChannel.open(heap.file.toPath, StandardOpenOption.READ)
    1.25 +      try {
    1.26 +        val len = file.size
    1.27 +        val n = sha1_prefix.length + SHA1.digest_length
    1.28 +        if (len >= n) {
    1.29 +          file.position(len - n)
    1.30 +
    1.31 +          val buf = ByteBuffer.allocate(n)
    1.32 +          var i = 0
    1.33 +          var m = 0
    1.34 +          do {
    1.35 +            m = file.read(buf)
    1.36 +            if (m != -1) i += m
    1.37 +          }
    1.38 +          while (m != -1 && n > i)
    1.39 +
    1.40 +          if (i == n) {
    1.41 +            val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
    1.42 +            val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
    1.43 +            if (prefix == sha1_prefix) Some(s) else None
    1.44 +          }
    1.45 +          else None
    1.46 +        }
    1.47 +        else None
    1.48 +      }
    1.49 +      finally { file.close }
    1.50 +    }
    1.51 +    else None
    1.52 +  }
    1.53 +
    1.54 +  def write_heap_digest(heap: Path): String =
    1.55 +    read_heap_digest(heap) match {
    1.56 +      case None =>
    1.57 +        val s = SHA1.digest(heap).rep
    1.58 +        File.append(heap, sha1_prefix + s)
    1.59 +        s
    1.60 +      case Some(s) => s
    1.61 +    }
    1.62 +
    1.63 +
    1.64 +
    1.65    /** persistent store **/
    1.66  
    1.67    def log(name: String): Path = Path.basic("log") + Path.basic(name)
    1.68 @@ -352,7 +403,7 @@
    1.69  
    1.70      def find(name: String): Option[(Path, Option[String])] =
    1.71        input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
    1.72 -        (dir + log_gz(name), File.time_stamp(dir + Path.basic(name))))
    1.73 +        (dir + log_gz(name), read_heap_digest(dir + Path.basic(name))))
    1.74  
    1.75      def find_log(name: String): Option[Path] =
    1.76        input_dirs.map(_ + log(name)).find(_.is_file)