equal
deleted
inserted
replaced
35 |
35 |
36 sealed case class Range(start: Offset, stop: Offset) |
36 sealed case class Range(start: Offset, stop: Offset) |
37 { |
37 { |
38 // denotation: {start} Un {i. start < i & i < stop} |
38 // denotation: {start} Un {i. start < i & i < stop} |
39 if (start > stop) |
39 if (start > stop) |
40 error("Bad range: [" + start.toString + ":" + stop.toString + "]") |
40 error("Bad range: [" + start.toString + ".." + stop.toString + "]") |
41 |
41 |
42 override def toString: String = "[" + start.toString + ":" + stop.toString + "]" |
42 override def toString: String = "[" + start.toString + ".." + stop.toString + "]" |
43 |
43 |
44 def length: Int = stop - start |
44 def length: Int = stop - start |
45 |
45 |
46 def map(f: Offset => Offset): Range = Range(f(start), f(stop)) |
46 def map(f: Offset => Offset): Range = Range(f(start), f(stop)) |
47 def +(i: Offset): Range = if (i == 0) this else map(_ + i) |
47 def +(i: Offset): Range = if (i == 0) this else map(_ + i) |