src/Pure/General/bytes.scala
changeset 62527 aae9a2a855e0
parent 60833 d201996f72a8
child 63779 9da65bc75610
equal deleted inserted replaced
62526:347150095fd2 62527:aae9a2a855e0
    18   def apply(s: CharSequence): Bytes =
    18   def apply(s: CharSequence): Bytes =
    19   {
    19   {
    20     val str = s.toString
    20     val str = s.toString
    21     if (str.isEmpty) empty
    21     if (str.isEmpty) empty
    22     else {
    22     else {
    23       val b = str.getBytes(UTF8.charset)
    23       val b = UTF8.bytes(str)
    24       new Bytes(b, 0, b.length)
    24       new Bytes(b, 0, b.length)
    25     }
    25     }
    26   }
    26   }
    27 
    27 
    28   def apply(a: Array[Byte], offset: Int, length: Int): Bytes =
    28   def apply(a: Array[Byte], offset: Int, length: Int): Bytes =