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