# HG changeset patch
# User wenzelm
# Date 1521315159 -3600
# Node ID cd00999d2d30c166217a077849f0041003730708
# Parent  fee080c4045fa34d48a8ac49d080664f4c156e16
more position information;

diff -r fee080c4045f -r cd00999d2d30 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sat Mar 17 18:30:13 2018 +0100
+++ b/src/Pure/Isar/token.scala	Sat Mar 17 20:32:39 2018 +0100
@@ -209,11 +209,12 @@
     def column = 0
     def lineContents = ""
 
-    def advance(token: Token): Pos =
+    def advance(token: Token): Pos = advance(token.source)
+    def advance(source: String): Pos =
     {
       var line1 = line
       var offset1 = offset
-      for (s <- Symbol.iterator(token.source)) {
+      for (s <- Symbol.iterator(source)) {
         if (line1 > 0 && Symbol.is_newline(s)) line1 += 1
         if (offset1 > 0) offset1 += 1
       }
@@ -230,6 +231,7 @@
 
     def position(): Position.T = position(0)
     def position(token: Token): Position.T = position(advance(token).offset)
+    def position(source: String): Position.T = position(advance(source).offset)
 
     override def toString: String = Position.here(position(), delimited = false)
   }
diff -r fee080c4045f -r cd00999d2d30 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Sat Mar 17 18:30:13 2018 +0100
+++ b/src/Pure/PIDE/command_span.scala	Sat Mar 17 20:32:39 2018 +0100
@@ -32,6 +32,13 @@
     def position: Position.T =
       kind match { case Command_Span(_, pos) => pos case _ => Position.none }
 
+    def keyword_pos(start: Token.Pos): Token.Pos =
+      kind match {
+        case _: Command_Span =>
+          (start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_))
+        case _ => start
+      }
+
     def is_begin: Boolean = content.exists(_.is_begin)
     def is_end: Boolean = content.exists(_.is_end)
 
diff -r fee080c4045f -r cd00999d2d30 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
     }