src/Pure/PIDE/text.scala
changeset 43425 0a5612040a8b
parent 38725 3d9d5ff80f6f
child 43428 b41dea5772c6
     1.1 --- a/src/Pure/PIDE/text.scala	Fri Jun 17 14:35:24 2011 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Fri Jun 17 23:18:22 2011 +0200
     1.3 @@ -25,7 +25,8 @@
     1.4    sealed case class Range(val start: Offset, val stop: Offset)
     1.5    {
     1.6      // denotation: {start} Un {i. start < i & i < stop}
     1.7 -    require(start <= stop)
     1.8 +    if (start > stop)
     1.9 +      error("Bad range: [" + start.toString + ":" + stop.toString + "]")
    1.10  
    1.11      override def toString = "[" + start.toString + ":" + stop.toString + "]"
    1.12  
    1.13 @@ -71,11 +72,13 @@
    1.14  
    1.15      private def transform(do_insert: Boolean, i: Offset): Offset =
    1.16        if (i < start) i
    1.17 -      else if (is_insert == do_insert) i + text.length
    1.18 +      else if (do_insert) i + text.length
    1.19        else (i - text.length) max start
    1.20  
    1.21 -    def convert(i: Offset): Offset = transform(true, i)
    1.22 -    def revert(i: Offset): Offset = transform(false, i)
    1.23 +    def convert(i: Offset): Offset = transform(is_insert, i)
    1.24 +    def revert(i: Offset): Offset = transform(!is_insert, i)
    1.25 +    def convert(range: Range): Range = range.map(convert)
    1.26 +    def revert(range: Range): Range = range.map(revert)
    1.27  
    1.28  
    1.29      /* edit strings */