digesting strings according to SHA-1 -- Scala version;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sha1.scala	Tue Aug 17 23:23:29 2010 +0200
@@ -0,0 +1,28 @@
+/*  Title:      Pure/General/sha1.scala
+    Author:     Makarius
+
+Digesting strings according to SHA-1 (see RFC 3174).
+*/
+
+package isabelle
+
+
+import java.security.MessageDigest
+
+
+object SHA1
+{
+  def digest_bytes(bytes: Array[Byte]): String =
+  {
+    val result = new StringBuilder
+    for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
+      val i = b.asInstanceOf[Int] & 0xFF
+      if (i < 16) result += '0'
+      result ++= Integer.toHexString(i)
+    }
+    result.toString
+  }
+
+  def digest(s: String): String = digest_bytes(Standard_System.string_bytes(s))
+}
+

--- a/src/Pure/build-jars	Tue Aug 17 23:00:51 2010 +0200
+++ b/src/Pure/build-jars	Tue Aug 17 23:23:29 2010 +0200
@@ -29,6 +29,7 @@
   General/position.scala
   General/pretty.scala
   General/scan.scala
+  General/sha1.scala
   General/symbol.scala
   General/xml.scala
   General/xml_data.scala