src/Pure/PIDE/text.scala
changeset 38577 4e4d3ea3725a
parent 38570 3fa11fb01f86
child 38578 1ebc6b76e5ff
     1.1 --- a/src/Pure/PIDE/text.scala	Sun Aug 22 16:43:20 2010 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Sun Aug 22 18:46:16 2010 +0200
     1.3 @@ -42,6 +42,15 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* information associated with text range */
     1.8 +
     1.9 +  case class Info[A](val range: Text.Range, val info: A)
    1.10 +  {
    1.11 +    def contains[B](that: Info[B]): Boolean = this.range contains that.range
    1.12 +    def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
    1.13 +  }
    1.14 +
    1.15 +
    1.16    /* editing */
    1.17  
    1.18    object Edit