equal
deleted
inserted
replaced
33 |
33 |
34 def advance(text: String, length: Length = Length): Position = |
34 def advance(text: String, length: Length = Length): Position = |
35 if (text.isEmpty) this |
35 if (text.isEmpty) this |
36 else { |
36 else { |
37 val lines = Library.split_lines(text) |
37 val lines = Library.split_lines(text) |
38 Position(line + lines.length - 1, column + length(Library.trim_line(lines.last))) |
38 val l = line + lines.length - 1 |
|
39 val c = (if (l == line) column else 0) + length(Library.trim_line(lines.last)) |
|
40 Position(l, c) |
39 } |
41 } |
40 } |
42 } |
41 |
43 |
42 |
44 |
43 /* range (right-open interval) */ |
45 /* range (right-open interval) */ |