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)