# HG changeset patch
# User wenzelm
# Date 1482516474 -3600
# Node ID f6c6e25ef782876e5cab3dc00c674535b9f9aa31
# Parent  00aa710ff7f06f35566d4d20ddac306bd3cf8cb6
tuned;

diff -r 00aa710ff7f0 -r f6c6e25ef782 src/Pure/PIDE/line.scala
--- 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)