src/Pure/PIDE/line.scala
changeset 64763 20e498a28f5e
parent 64701 931f51fb24ca
child 64800 415dafeb9669
--- 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