added reverse CharSequence;
authorwenzelm
Thu, 18 Jun 2009 14:02:47 +0200
changeset 31700 b44912113c83
parent 31699 b6710a3b4c49
child 31701 d3d2e417fb5e
added reverse CharSequence;
src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Thu Jun 18 00:00:52 2009 +0200
+++ b/src/Pure/General/scan.scala	Thu Jun 18 14:02:47 2009 +0200
@@ -136,5 +136,28 @@
     }.named("keyword")
 
   }
+
+
+  /** reverse CharSequence **/
+
+  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
+  {
+    require(0 <= start && start <= end && end <= text.length)
+
+    def this(text: CharSequence) = this(text, 0, text.length)
+
+    def length: Int = end - start
+    def charAt(i: Int): Char = text.charAt(end - i - 1)
+    def subSequence(i: Int, j: Int): CharSequence = new Reverse(text, end - j, end - i)
+
+    override def toString: String =
+    {
+      val buf = new StringBuffer(length)
+      for (i <- 0 until length)
+        buf.append(charAt(i))
+      buf.toString
+    }
+  }
+
 }