# HG changeset patch # User wenzelm # Date 1322227416 -3600 # Node ID 6bdf8b926f502fb02d977b2eb98d511a8e4f1599 # Parent 0dd654a01217090b06bc70ff0bc2b78f15df77e0 recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution; 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 }