src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Sat Mar 17 18:30:13 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Mar 17 20:32:39 2018 +0100
@@ -224,6 +224,17 @@
         }
       }
 
+      def starts_pos(commands: Iterator[Command], pos: Token.Pos = Token.Pos.start)
+        : Iterator[(Command, Token.Pos)] =
+      {
+        var p = pos
+        for (command <- commands) yield {
+          val start = p
+          p = (p /: command.span.content)(_.advance(_))
+          (command, start)
+        }
+      }
+
       private val block_size = 256
     }