equal
deleted
inserted
replaced
121 } |
121 } |
122 } |
122 } |
123 move(offset, 0, lines) |
123 move(offset, 0, lines) |
124 } |
124 } |
125 |
125 |
|
126 def range(text_range: Text.Range, length: Length = Length): Range = |
|
127 Range( |
|
128 position(text_range.start, length), |
|
129 position(text_range.stop, length)) |
|
130 |
126 def offset(pos: Position, length: Length = Length): Option[Text.Offset] = |
131 def offset(pos: Position, length: Length = Length): Option[Text.Offset] = |
127 { |
132 { |
128 val l = pos.line |
133 val l = pos.line |
129 val c = pos.column |
134 val c = pos.column |
130 if (0 <= l && l < lines.length) { |
135 if (0 <= l && l < lines.length) { |