diff -r 805c5e6fa430 -r bbfcef118acb src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala Wed Dec 21 16:32:34 2016 +0100 +++ b/src/Pure/PIDE/line.scala Wed Dec 21 21:17:44 2016 +0100 @@ -44,12 +44,19 @@ /* range (right-open interval) */ + object Range + { + val zero: Range = Range(Position.zero, Position.zero) + } + sealed case class Range(start: Position, stop: Position) { if (start.compare(stop) > 0) error("Bad line range: " + start.print + ".." + stop.print) - def print: String = start.print + ".." + stop.print + def print: String = + if (start == stop) start.print + else start.print + ".." + stop.print }