src/Pure/PIDE/line.scala
changeset 64666 f6c6e25ef782
parent 64651 ea5620f7b0d8
child 64672 d8e0619abb60
--- a/src/Pure/PIDE/line.scala	Fri Dec 23 17:04:29 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Fri Dec 23 19:07:54 2016 +0100
@@ -46,7 +46,8 @@
 
   object Range
   {
-    val zero: Range = Range(Position.zero, Position.zero)
+    def apply(start: Position): Range = Range(start, start)
+    val zero: Range = Range(Position.zero)
   }
 
   sealed case class Range(start: Position, stop: Position)