changeset 73559 | 22b5ecb53dd9 |
parent 73554 | c973b5300025 |
child 73561 | c83152933579 |
--- a/src/Pure/General/bytes.scala Sun Apr 11 21:32:09 2021 +0200 +++ b/src/Pure/General/bytes.scala Sun Apr 11 22:47:55 2021 +0200 @@ -135,7 +135,10 @@ } def text: String = - UTF8.decode_chars(s => s, bytes, offset, offset + length).toString + UTF8.decode_chars(identity, bytes, offset, offset + length).toString + + def symbols: String = + UTF8.decode_chars(Symbol.decode, bytes, offset, offset + length).toString def base64: String = {