diff -r f6c9a4f9f66f -r a6e2715fac5f src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Thu Aug 19 22:26:15 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Thu Aug 19 22:52:00 2010 +0200
@@ -38,7 +38,7 @@
     def start_range: Range = Range(start, start)
     def stop_range: Range = Range(stop, stop)
 
-    def intersect(that: Range): Range =
+    def restrict(that: Range): Range =
       Range(this.start max that.start, this.stop min that.stop)
   }