src/Pure/PIDE/text.scala
changeset 45631 6bdf8b926f50
parent 45470 81b85d4ed269
child 45667 546d78f0d81f
     1.1 --- a/src/Pure/PIDE/text.scala	Fri Nov 25 13:14:58 2011 +0100
     1.2 +++ b/src/Pure/PIDE/text.scala	Fri Nov 25 14:23:36 2011 +0100
     1.3 @@ -101,6 +101,13 @@
     1.4      def range: Range =
     1.5        if (is_empty) Range(0)
     1.6        else Range(ranges.head.start, ranges.last.stop)
     1.7 +
     1.8 +    override def hashCode: Int = ranges.hashCode
     1.9 +    override def equals(that: Any): Boolean =
    1.10 +      that match {
    1.11 +        case other: Perspective => ranges == other.ranges
    1.12 +        case _ => false
    1.13 +      }
    1.14      override def toString = ranges.toString
    1.15    }
    1.16