proper reset of column (amending 01e50039edc9);
authorwenzelm
Tue Dec 20 17:46:44 2016 +0100 (2016-12-20)
changeset 64619e3d9a31281f3
parent 64618 c81bd30839a6
child 64620 14f938969779
proper reset of column (amending 01e50039edc9);
src/Pure/PIDE/line.scala
     1.1 --- a/src/Pure/PIDE/line.scala	Tue Dec 20 17:09:40 2016 +0100
     1.2 +++ b/src/Pure/PIDE/line.scala	Tue Dec 20 17:46:44 2016 +0100
     1.3 @@ -35,7 +35,9 @@
     1.4        if (text.isEmpty) this
     1.5        else {
     1.6          val lines = Library.split_lines(text)
     1.7 -        Position(line + lines.length - 1, column + length(Library.trim_line(lines.last)))
     1.8 +        val l = line + lines.length - 1
     1.9 +        val c = (if (l == line) column else 0) + length(Library.trim_line(lines.last))
    1.10 +        Position(l, c)
    1.11        }
    1.12    }
    1.13