equal
deleted
inserted
replaced
123 { |
123 { |
124 val l = pos.line |
124 val l = pos.line |
125 val c = pos.column |
125 val c = pos.column |
126 if (0 <= l && l < lines.length) { |
126 if (0 <= l && l < lines.length) { |
127 val line_offset = |
127 val line_offset = |
128 if (l == 0) 0 |
128 (0 /: lines.iterator.take(l)) { case (n, line) => n + text_length(line.text) + 1 } |
129 else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 } |
|
130 text_length.offset(lines(l).text, c).map(line_offset + _) |
129 text_length.offset(lines(l).text, c).map(line_offset + _) |
131 } |
130 } |
132 else None |
131 else None |
133 } |
132 } |
134 |
133 |