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)
   }