equal
deleted
inserted
replaced
152 else if (do_insert) i + text.length |
152 else if (do_insert) i + text.length |
153 else (i - text.length) max start |
153 else (i - text.length) max start |
154 |
154 |
155 def convert(i: Offset): Offset = transform(is_insert, i) |
155 def convert(i: Offset): Offset = transform(is_insert, i) |
156 def revert(i: Offset): Offset = transform(!is_insert, i) |
156 def revert(i: Offset): Offset = transform(!is_insert, i) |
157 def convert(range: Range): Range = range.map(convert) |
|
158 def revert(range: Range): Range = range.map(revert) |
|
159 |
157 |
160 |
158 |
161 /* edit strings */ |
159 /* edit strings */ |
162 |
160 |
163 private def insert(i: Offset, string: String): String = |
161 private def insert(i: Offset, string: String): String = |