src/Pure/System/standard_system.scala

--- a/src/Pure/System/standard_system.scala	Mon Jul 11 10:27:50 2011 +0200
+++ b/src/Pure/System/standard_system.scala	Mon Jul 11 11:13:33 2011 +0200
@@ -79,6 +79,25 @@
     buf.toString
   }
 
+  private class Decode_Chars(decode: String => String,
+    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
+  {
+    def length: Int = end - start
+    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
+    def subSequence(i: Int, j: Int): CharSequence =
+      new Decode_Chars(decode, buffer, start + i, start + j)
+
+    // toString with adhoc decoding: abuse of CharSequence interface
+    override def toString: String = decode(decode_permissive_utf8(this))
+  }
+
+  def decode_chars(decode: String => String,
+    buffer: Array[Byte], start: Int, end: Int): CharSequence =
+  {
+    require(0 <= start && start <= end && end <= buffer.length)
+    new Decode_Chars(decode, buffer, start, end)
+  }
+
 
   /* basic file operations */