author | wenzelm |
Tue, 03 Jan 2017 17:21:37 +0100 | |
changeset 64763 | 20e498a28f5e |
parent 64762 | cd545bec3fd0 |
child 64764 | 452b4fb7927c |
--- a/src/Pure/PIDE/line.scala Tue Jan 03 15:21:32 2017 +0100 +++ b/src/Pure/PIDE/line.scala Tue Jan 03 17:21:37 2017 +0100 @@ -125,8 +125,7 @@ val c = pos.column if (0 <= l && l < lines.length) { val line_offset = - if (l == 0) 0 - else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 } + (0 /: lines.iterator.take(l)) { case (n, line) => n + text_length(line.text) + 1 } text_length.offset(lines(l).text, c).map(line_offset + _) } else None