# HG changeset patch
# User wenzelm
# Date 1483460497 -3600
# Node ID 20e498a28f5e39a767ea0dd21cdadd0b15a33eac
# Parent  cd545bec3fd016a2db8c7a1f20bef489a13a9acf
proper line_offset;

diff -r cd545bec3fd0 -r 20e498a28f5e src/Pure/PIDE/line.scala
--- 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