src/Pure/General/bytes.scala
changeset 73559 22b5ecb53dd9
parent 73554 c973b5300025
child 73561 c83152933579
equal deleted inserted replaced
73558:a5d1d1e2f109 73559:22b5ecb53dd9
   133     System.arraycopy(bytes, offset, a, 0, length)
   133     System.arraycopy(bytes, offset, a, 0, length)
   134     a
   134     a
   135   }
   135   }
   136 
   136 
   137   def text: String =
   137   def text: String =
   138     UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
   138     UTF8.decode_chars(identity, bytes, offset, offset + length).toString
       
   139 
       
   140   def symbols: String =
       
   141     UTF8.decode_chars(Symbol.decode, bytes, offset, offset + length).toString
   139 
   142 
   140   def base64: String =
   143   def base64: String =
   141   {
   144   {
   142     val b =
   145     val b =
   143       if (offset == 0 && length == bytes.length) bytes
   146       if (offset == 0 && length == bytes.length) bytes