equal
deleted
inserted
replaced
39 |
39 |
40 sealed case class Range(start: Offset, stop: Offset) |
40 sealed case class Range(start: Offset, stop: Offset) |
41 { |
41 { |
42 // denotation: {start} Un {i. start < i & i < stop} |
42 // denotation: {start} Un {i. start < i & i < stop} |
43 if (start > stop) |
43 if (start > stop) |
44 error("Bad range: [" + start.toString + ":" + stop.toString + "]") |
44 Console.printf("Bad range: [" + start.toString + ":" + stop.toString + "]") |
45 |
45 |
46 override def toString: String = "[" + start.toString + ":" + stop.toString + "]" |
46 override def toString: String = "[" + start.toString + ":" + stop.toString + "]" |
47 |
47 |
48 def length: Int = stop - start |
48 def length: Int = stop - start |
49 |
49 |