# HG changeset patch
# User wenzelm
# Date 1342637942 -7200
# Node ID 3060e6343953491ad77fc4a87ffa98a028ec4b72
# Parent  4a8f06cbf8bbb8a5d4bf5d8bbb22da17a9d28715
more SHA1.digest operations;

diff -r 4a8f06cbf8bb -r 3060e6343953 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Wed Jul 18 20:55:19 2012 +0200
+++ b/src/Pure/General/sha1.scala	Wed Jul 18 20:59:02 2012 +0200
@@ -8,6 +8,7 @@
 package isabelle
 
 
+import java.io.{File, FileInputStream}
 import java.security.MessageDigest
 
 
@@ -18,10 +19,10 @@
     override def toString: String = rep
   }
 
-  def digest_bytes(bytes: Array[Byte]): Digest =
+  private def make_result(digest: MessageDigest): Digest =
   {
     val result = new StringBuilder
-    for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
+    for (b <- digest.digest()) {
       val i = b.asInstanceOf[Int] & 0xFF
       if (i < 16) result += '0'
       result ++= Integer.toHexString(i)
@@ -29,6 +30,32 @@
     Digest(result.toString)
   }
 
-  def digest(s: String): Digest = digest_bytes(Standard_System.string_bytes(s))
+  def digest(file: File): Digest =
+  {
+    val stream = new FileInputStream(file)
+    val digest = MessageDigest.getInstance("SHA")
+
+    val buf = new Array[Byte](65536)
+    var m = 0
+    try {
+      do {
+        m = stream.read(buf, 0, buf.length)
+        if (m != -1) digest.update(buf, 0, m)
+      } while (m != -1)
+    }
+    finally { stream.close }
+
+    make_result(digest)
+  }
+
+  def digest(bytes: Array[Byte]): Digest =
+  {
+    val digest = MessageDigest.getInstance("SHA")
+    digest.update(bytes)
+
+    make_result(digest)
+  }
+
+  def digest(string: String): Digest = digest(Standard_System.string_bytes(string))
 }