tuned signature;
authorwenzelm
Thu, 24 Mar 2016 13:08:12 +0100
changeset 62702 e29f47e04180
parent 62701 715bf5beedc0
child 62703 01b71da798dd
tuned signature;
src/Pure/General/sha1.ML
src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.ML	Wed Mar 23 09:37:38 2016 +1100
+++ b/src/Pure/General/sha1.ML	Thu Mar 24 13:08:12 2016 +0100
@@ -8,9 +8,9 @@
 signature SHA1 =
 sig
   eqtype digest
-  val digest: string -> digest
   val rep: digest -> string
   val fake: string -> digest
+  val digest: string -> digest
   val test_samples: unit -> unit
 end;
 
--- a/src/Pure/General/sha1.scala	Wed Mar 23 09:37:38 2016 +1100
+++ b/src/Pure/General/sha1.scala	Thu Mar 24 13:08:12 2016 +0100
@@ -36,6 +36,8 @@
     new Digest(result.toString)
   }
 
+  def fake(rep: String): Digest = new Digest(rep)
+
   def digest(file: JFile): Digest =
   {
     val stream = new FileInputStream(file)
@@ -63,9 +65,7 @@
   }
 
   def digest(bytes: Bytes): Digest = bytes.sha1_digest
-
   def digest(string: String): Digest = digest(Bytes(string))
 
-  def fake(rep: String): Digest = new Digest(rep)
+  val digest_length: Int = digest("").rep.length
 }
-