author | wenzelm |
Tue, 20 Dec 2016 17:46:44 +0100 | |
changeset 64619 | e3d9a31281f3 |
parent 64618 | c81bd30839a6 |
child 64620 | 14f938969779 |
--- a/src/Pure/PIDE/line.scala Tue Dec 20 17:09:40 2016 +0100 +++ b/src/Pure/PIDE/line.scala Tue Dec 20 17:46:44 2016 +0100 @@ -35,7 +35,9 @@ if (text.isEmpty) this else { val lines = Library.split_lines(text) - Position(line + lines.length - 1, column + length(Library.trim_line(lines.last))) + val l = line + lines.length - 1 + val c = (if (l == line) column else 0) + length(Library.trim_line(lines.last)) + Position(l, c) } }