prefer UTF8.decode_permissive;

--- 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
 

--- 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 =
   {