src/Pure/Isar/outer_syntax.scala

   def parse_spans(toks: List[Token]): List[Command_Span.Span] =
   {
     val result = new mutable.ListBuffer[Command_Span.Span]
     val content = new mutable.ListBuffer[Token]
     val ignored = new mutable.ListBuffer[Token]
-    var start = 0
 
     def ship(content: List[Token])
     {
       val kind =
         if (content.forall(_.is_ignored)) Command_Span.Ignored_Span

               val offset =
                 (0 /: content.takeWhile(_ != cmd)) {
                   case (i, tok) => i + Symbol.length(tok.source) }
               val end_offset = offset + Symbol.length(name)
               val range = Text.Range(offset, end_offset) + 1
-              val pos = Position.Range(range)
-              val abs_pos = Position.Range(range + start)
-              Command_Span.Command_Span(name, pos, abs_pos)
+              Command_Span.Command_Span(name, Position.Range(range))
           }
-      for (tok <- content) start += Symbol.length(tok.source)
       result += Command_Span.Span(kind, content)
     }
 
     def flush()
     {