src/Pure/General/bytes.scala
changeset 80360 6ea999f55c2d
parent 80359 bb4e95d19ecb
child 80361 54a83e8e447b
equal deleted inserted replaced
80359:bb4e95d19ecb 80360:6ea999f55c2d
   156 
   156 
   157 
   157 
   158   /* content */
   158   /* content */
   159 
   159 
   160   lazy val sha1_digest: SHA1.Digest =
   160   lazy val sha1_digest: SHA1.Digest =
   161     if (is_empty) SHA1.digest_empty
   161     if (is_empty) SHA1.digest_empty else SHA1.digest(bytes, offset, length)
   162     else SHA1.make_digest { sha => sha.update(bytes, offset, length) }
       
   163 
   162 
   164   def is_empty: Boolean = length == 0
   163   def is_empty: Boolean = length == 0
   165 
   164 
   166   def iterator: Iterator[Byte] =
   165   def iterator: Iterator[Byte] =
   167     for (i <- (offset until (offset + length)).iterator)
   166     for (i <- (offset until (offset + length)).iterator)