author | wenzelm |
Fri, 23 Dec 2016 19:07:54 +0100 | |
changeset 64666 | f6c6e25ef782 |
parent 64665 | 00aa710ff7f0 |
child 64667 | cdb0d559a24b |
--- 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)