diff -r 7f87c1aa0ffa -r 642b6105e6f4 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Dec 28 16:50:14 2016 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Dec 28 17:02:38 2016 +0100
@@ -808,7 +808,7 @@
               node.commands.iterator.takeWhile(_ != command).map(_.source) ++
                 (if (offset == 0) Iterator.empty
                  else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
-            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_, Length))
             Line.Node_Position(name, pos)
           }