# HG changeset patch # User wenzelm # Date 1282814983 -7200 # Node ID 3d9d5ff80f6f77c578085dc46b3707d351a501f5 # Parent d1feec02cf0205a826542c2cf7a39f2e457aee22 tuned signature; diff -r d1feec02cf02 -r 3d9d5ff80f6f src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Wed Aug 25 22:57:40 2010 +0200 +++ b/src/Pure/PIDE/text.scala Thu Aug 26 11:29:43 2010 +0200 @@ -33,7 +33,7 @@ def +(i: Offset): Range = map(_ + i) def -(i: Offset): Range = map(_ - i) - def is_singleton: Boolean = start == stop + def is_singularity: Boolean = start == stop def contains(i: Offset): Boolean = start == i || start < i && i < stop def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop