recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
--- 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
}