# HG changeset patch
# User wenzelm
# Date 1384602076 -3600
# Node ID a2290f36d1d65a030fc999eb2b575d52945e5bbb
# Parent  9714b5474f391b71022d572f4cd659bc2c2c2750
prefer UTF8.decode_permissive;

diff -r 9714b5474f39 -r a2290f36d1d6 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Nov 16 12:29:10 2013 +0100
+++ b/src/Pure/General/bytes.scala	Sat Nov 16 12:41:16 2013 +0100
@@ -91,7 +91,8 @@
 
   def sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
-  override def toString: String = new String(bytes, offset, length, UTF8.charset)
+  override def toString: String =
+    UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
 
   def isEmpty: Boolean = length == 0
 
diff -r 9714b5474f39 -r a2290f36d1d6 src/Pure/System/utf8.scala
--- a/src/Pure/System/utf8.scala	Sat Nov 16 12:29:10 2013 +0100
+++ b/src/Pure/System/utf8.scala	Sat Nov 16 12:41:16 2013 +0100
@@ -24,7 +24,7 @@
   /* permissive UTF-8 decoding */
 
   // see also http://en.wikipedia.org/wiki/UTF-8#Description
-  // overlong encodings enable byte-stuffing
+  // overlong encodings enable byte-stuffing of low-ASCII
 
   def decode_permissive(text: CharSequence): String =
   {