# HG changeset patch
# User wenzelm
# Date 1245330138 -7200
# Node ID d3d2e417fb5e96bf807428aeddf8c3e3e2bf2c88
# Parent  b44912113c83f73939652ca75acc1fff107779b3
subSequence: bounds checking;

diff -r b44912113c83 -r d3d2e417fb5e src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Thu Jun 18 14:02:47 2009 +0200
+++ b/src/Pure/General/scan.scala	Thu Jun 18 15:02:18 2009 +0200
@@ -148,7 +148,10 @@
 
     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)
+
+    def subSequence(i: Int, j: Int): CharSequence =
+      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
+      else throw new IndexOutOfBoundsException
 
     override def toString: String =
     {