--- a/src/Pure/PIDE/document.scala Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/PIDE/document.scala Wed Dec 28 17:10:09 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(_, Length))
+ val pos = (Line.Position.zero /: sources_iterator)(_.advance(_, Text.Length))
Line.Node_Position(name, pos)
}