more position information;
authorwenzelm
Sat Mar 17 20:32:39 2018 +0100 (16 months ago)
changeset 67895cd00999d2d30
parent 67894 fee080c4045f
child 67896 00797fb82869
more position information;
src/Pure/Isar/token.scala
src/Pure/PIDE/command_span.scala
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/Isar/token.scala	Sat Mar 17 18:30:13 2018 +0100
     1.2 +++ b/src/Pure/Isar/token.scala	Sat Mar 17 20:32:39 2018 +0100
     1.3 @@ -209,11 +209,12 @@
     1.4      def column = 0
     1.5      def lineContents = ""
     1.6  
     1.7 -    def advance(token: Token): Pos =
     1.8 +    def advance(token: Token): Pos = advance(token.source)
     1.9 +    def advance(source: String): Pos =
    1.10      {
    1.11        var line1 = line
    1.12        var offset1 = offset
    1.13 -      for (s <- Symbol.iterator(token.source)) {
    1.14 +      for (s <- Symbol.iterator(source)) {
    1.15          if (line1 > 0 && Symbol.is_newline(s)) line1 += 1
    1.16          if (offset1 > 0) offset1 += 1
    1.17        }
    1.18 @@ -230,6 +231,7 @@
    1.19  
    1.20      def position(): Position.T = position(0)
    1.21      def position(token: Token): Position.T = position(advance(token).offset)
    1.22 +    def position(source: String): Position.T = position(advance(source).offset)
    1.23  
    1.24      override def toString: String = Position.here(position(), delimited = false)
    1.25    }
     2.1 --- a/src/Pure/PIDE/command_span.scala	Sat Mar 17 18:30:13 2018 +0100
     2.2 +++ b/src/Pure/PIDE/command_span.scala	Sat Mar 17 20:32:39 2018 +0100
     2.3 @@ -32,6 +32,13 @@
     2.4      def position: Position.T =
     2.5        kind match { case Command_Span(_, pos) => pos case _ => Position.none }
     2.6  
     2.7 +    def keyword_pos(start: Token.Pos): Token.Pos =
     2.8 +      kind match {
     2.9 +        case _: Command_Span =>
    2.10 +          (start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_))
    2.11 +        case _ => start
    2.12 +      }
    2.13 +
    2.14      def is_begin: Boolean = content.exists(_.is_begin)
    2.15      def is_end: Boolean = content.exists(_.is_end)
    2.16  
     3.1 --- a/src/Pure/PIDE/document.scala	Sat Mar 17 18:30:13 2018 +0100
     3.2 +++ b/src/Pure/PIDE/document.scala	Sat Mar 17 20:32:39 2018 +0100
     3.3 @@ -224,6 +224,17 @@
     3.4          }
     3.5        }
     3.6  
     3.7 +      def starts_pos(commands: Iterator[Command], pos: Token.Pos = Token.Pos.start)
     3.8 +        : Iterator[(Command, Token.Pos)] =
     3.9 +      {
    3.10 +        var p = pos
    3.11 +        for (command <- commands) yield {
    3.12 +          val start = p
    3.13 +          p = (p /: command.span.content)(_.advance(_))
    3.14 +          (command, start)
    3.15 +        }
    3.16 +      }
    3.17 +
    3.18        private val block_size = 256
    3.19      }
    3.20