src/Pure/General/bytes.scala
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 =
   {