| changeset 38578 | 1ebc6b76e5ff |
| parent 38577 | 4e4d3ea3725a |
| child 38662 | 4d4553e09337 |
--- a/src/Pure/PIDE/text.scala Sun Aug 22 18:46:16 2010 +0200 +++ b/src/Pure/PIDE/text.scala Sun Aug 22 19:33:01 2010 +0200 @@ -46,7 +46,6 @@ case class Info[A](val range: Text.Range, val info: A) { - def contains[B](that: Info[B]): Boolean = this.range contains that.range def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info) }