diff -r 0dd654a01217 -r 6bdf8b926f50 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Fri Nov 25 13:14:58 2011 +0100
+++ b/src/Pure/PIDE/text.scala	Fri Nov 25 14:23:36 2011 +0100
@@ -101,6 +101,13 @@
     def range: Range =
       if (is_empty) Range(0)
       else Range(ranges.head.start, ranges.last.stop)
+
+    override def hashCode: Int = ranges.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Perspective => ranges == other.ranges
+        case _ => false
+      }
     override def toString = ranges.toString
   }