src/Pure/PIDE/text.scala
changeset 38427 7066fbd315ae
parent 38426 2858ec7b6dd8
child 38477 f01f4ab2a0af
     1.1 --- a/src/Pure/PIDE/text.scala	Sun Aug 15 22:48:56 2010 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Sun Aug 15 23:07:22 2010 +0200
     1.3 @@ -15,6 +15,11 @@
     1.4    type Offset = Int
     1.5  
     1.6    sealed case class Range(val start: Offset, val stop: Offset)
     1.7 +  {
     1.8 +    def contains(i: Offset): Boolean = start <= i && i < stop
     1.9 +    def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    1.10 +    def +(i: Offset): Range = map(_ + i)
    1.11 +  }
    1.12  
    1.13  
    1.14    /* editing */