diff --git a/src/Pure/Isar/outer_syntax.scala b/src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala
+++ b/src/Pure/Isar/outer_syntax.scala
@@ -1,210 +1,214 @@
 /*  Title:      Pure/Isar/outer_syntax.scala
     Author:     Makarius
 
 Isabelle/Isar outer syntax.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 
 
 object Outer_Syntax
 {
   /* syntax */
 
   val empty: Outer_Syntax = new Outer_Syntax()
 
   def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
 
 
   /* string literals */
 
   def quote_string(str: String): String =
   {
     val result = new StringBuilder(str.length + 10)
     result += '"'
     for (s <- Symbol.iterator(str)) {
       if (s.length == 1) {
         val c = s(0)
         if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
           result += '\\'
           if (c < 10) result += '0'
           if (c < 100) result += '0'
           result ++= c.asInstanceOf[Int].toString
         }
         else result += c
       }
       else result ++= s
     }
     result += '"'
     result.toString
   }
 }
 
 final class Outer_Syntax private(
   val keywords: Keyword.Keywords = Keyword.Keywords.empty,
   val rev_abbrevs: Thy_Header.Abbrevs = Nil,
   val language_context: Completion.Language_Context = Completion.Language_Context.outer,
   val has_tokens: Boolean = true)
 {
   /** syntax content **/
 
   override def toString: String = keywords.toString
 
 
   /* keywords */
 
   def + (name: String, kind: String = "", load_command: String = ""): Outer_Syntax =
     new Outer_Syntax(
       keywords + (name, kind, load_command), rev_abbrevs, language_context, has_tokens = true)
 
   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
     (this /: keywords) {
       case (syntax, (name, spec)) =>
         syntax +
           (Symbol.decode(name), spec.kind, spec.load_command) +
           (Symbol.encode(name), spec.kind, spec.load_command)
     }
 
 
   /* abbrevs */
 
   def abbrevs: Thy_Header.Abbrevs = rev_abbrevs.reverse
 
   def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
     if (new_abbrevs.isEmpty) this
     else {
       val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
       new Outer_Syntax(keywords, rev_abbrevs1, language_context, has_tokens)
     }
 
 
   /* completion */
 
   private lazy val completion: Completion =
   {
     val completion_keywords = (keywords.minor.iterator ++ keywords.major.iterator).toList
     val completion_abbrevs =
       completion_keywords.flatMap(name =>
         (if (Keyword.theory_block.contains(keywords.kinds(name)))
           List((name, name + "\nbegin\n\u0007\nend"))
          else Nil) :::
         (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil)) :::
       abbrevs.flatMap(
         { case (a, b) =>
             val a1 = Symbol.decode(a)
             val a2 = Symbol.encode(a)
             val b1 = Symbol.decode(b)
             List((a1, b1), (a2, b1))
         })
     Completion.make(completion_keywords, completion_abbrevs)
   }
 
   def complete(
     history: Completion.History,
     unicode: Boolean,
     explicit: Boolean,
     start: Text.Offset,
     text: CharSequence,
     caret: Int,
     context: Completion.Language_Context): Option[Completion.Result] =
   {
     completion.complete(history, unicode, explicit, start, text, caret, context)
   }
 
 
   /* build */
 
   def + (header: Document.Node.Header): Outer_Syntax =
     add_keywords(header.keywords).add_abbrevs(header.abbrevs)
 
   def ++ (other: Outer_Syntax): Outer_Syntax =
     if (this eq other) this
     else if (this eq Outer_Syntax.empty) other
     else {
       val keywords1 = keywords ++ other.keywords
       val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs)
       if ((keywords eq keywords1) && (rev_abbrevs eq rev_abbrevs1)) this
       else new Outer_Syntax(keywords1, rev_abbrevs1, language_context, has_tokens)
     }
 
 
   /* load commands */
 
   def load_command(name: String): Option[String] =
     keywords.load_commands.get(name)
 
   def has_load_commands(text: String): Boolean =
     keywords.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
 
 
   /* language context */
 
   def set_language_context(context: Completion.Language_Context): Outer_Syntax =
     new Outer_Syntax(keywords, rev_abbrevs, context, has_tokens)
 
   def no_tokens: Outer_Syntax =
   {
     require(keywords.is_empty)
     new Outer_Syntax(
       rev_abbrevs = rev_abbrevs,
       language_context = language_context,
       has_tokens = false)
   }
 
 
 
   /** parsing **/
 
   /* command spans */
 
   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(span: List[Token])
+    def ship(content: List[Token])
     {
       val kind =
-        if (span.forall(_.is_ignored)) Command_Span.Ignored_Span
-        else if (span.exists(_.is_error)) Command_Span.Malformed_Span
+        if (content.forall(_.is_ignored)) Command_Span.Ignored_Span
+        else if (content.exists(_.is_error)) Command_Span.Malformed_Span
         else
-          span.find(_.is_command) match {
+          content.find(_.is_command) match {
             case None => Command_Span.Malformed_Span
             case Some(cmd) =>
               val name = cmd.source
               val offset =
-                (0 /: span.takeWhile(_ != cmd)) {
+                (0 /: content.takeWhile(_ != cmd)) {
                   case (i, tok) => i + Symbol.length(tok.source) }
               val end_offset = offset + Symbol.length(name)
-              val pos = Position.Range(Text.Range(offset, end_offset) + 1)
-              Command_Span.Command_Span(name, pos)
+              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)
           }
-      result += Command_Span.Span(kind, span)
+      for (tok <- content) start += Symbol.length(tok.source)
+      result += Command_Span.Span(kind, content)
     }
 
     def flush()
     {
       if (content.nonEmpty) { ship(content.toList); content.clear }
       if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear }
     }
 
     for (tok <- toks) {
       if (tok.is_ignored) ignored += tok
       else if (keywords.is_before_command(tok) ||
         tok.is_command &&
           (!content.exists(keywords.is_before_command) || content.exists(_.is_command)))
       { flush(); content += tok }
       else { content ++= ignored; ignored.clear; content += tok }
     }
     flush()
 
     result.toList
   }
 
   def parse_spans(input: CharSequence): List[Command_Span.Span] =
     parse_spans(Token.explode(keywords, input))
 }
diff --git a/src/Pure/PIDE/command_span.scala b/src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala
+++ b/src/Pure/PIDE/command_span.scala
@@ -1,140 +1,143 @@
 /*  Title:      Pure/PIDE/command_span.scala
     Author:     Makarius
 
 Syntactic representation of command spans.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 
 
 object Command_Span
 {
   /* loaded files */
 
   object Loaded_Files
   {
     val none: Loaded_Files = Loaded_Files(Nil, -1)
   }
   sealed case class Loaded_Files(files: List[String], index: Int)
 
   class Load_Command(val name: String) extends Isabelle_System.Service
   {
     override def toString: String = name
 
     def extensions: List[String] = Nil
 
     def loaded_files(tokens: List[(Token, Int)]): Loaded_Files =
       tokens.collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) match {
         case Some((file, i)) =>
           extensions match {
             case Nil => Loaded_Files(List(file), i)
             case exts => Loaded_Files(exts.map(ext => file + "." + ext), i)
           }
         case None => Loaded_Files.none
       }
   }
 
   lazy val load_commands: List[Load_Command] =
     new Load_Command("") :: Isabelle_System.make_services(classOf[Load_Command])
 
 
   /* span kind */
 
   sealed abstract class Kind {
     override def toString: String =
       this match {
-        case Command_Span(name, _) => proper_string(name) getOrElse "<command>"
+        case Command_Span(name, _, _) => proper_string(name) getOrElse "<command>"
         case Ignored_Span => "<ignored>"
         case Malformed_Span => "<malformed>"
         case Theory_Span => "<theory>"
       }
   }
-  case class Command_Span(name: String, pos: Position.T) extends Kind
+  case class Command_Span(name: String, pos: Position.T, abs_pos: Position.T) extends Kind
   case object Ignored_Span extends Kind
   case object Malformed_Span extends Kind
   case object Theory_Span extends Kind
 
 
   /* span */
 
   sealed case class Span(kind: Kind, content: List[Token])
   {
     def is_theory: Boolean = kind == Theory_Span
 
     def name: String =
-      kind match { case Command_Span(name, _) => name case _ => "" }
+      kind match { case k: Command_Span => k.name case _ => "" }
 
     def position: Position.T =
-      kind match { case Command_Span(_, pos) => pos case _ => Position.none }
+      kind match { case k: Command_Span => k.pos case _ => Position.none }
+
+    def absolute_position: Position.T =
+      kind match { case k: Command_Span => k.abs_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_kind(keywords: Keyword.Keywords, pred: String => Boolean, other: Boolean): Boolean =
       keywords.kinds.get(name) match {
         case Some(k) => pred(k)
         case None => other
       }
 
     def is_begin: Boolean = content.exists(_.is_begin)
     def is_end: Boolean = content.exists(_.is_end)
 
     def length: Int = (0 /: content)(_ + _.source.length)
 
     def compact_source: (String, Span) =
     {
       val source = Token.implode(content)
       val content1 = new mutable.ListBuffer[Token]
       var i = 0
       for (Token(kind, s) <- content) {
         val n = s.length
         val s1 = source.substring(i, i + n)
         content1 += Token(kind, s1)
         i += n
       }
       (source, Span(kind, content1.toList))
     }
 
     def clean_arguments: List[(Token, Int)] =
     {
       if (name.nonEmpty) {
         def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
           toks match {
             case (t1, i1) :: (t2, i2) :: rest =>
               if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
               else (t1, i1) :: clean((t2, i2) :: rest)
             case _ => toks
           }
         clean(content.zipWithIndex.filter({ case (t, _) => t.is_proper }))
           .dropWhile({ case (t, _) => !t.is_command })
           .dropWhile({ case (t, _) => t.is_command })
       }
       else Nil
     }
 
     def loaded_files(syntax: Outer_Syntax): Loaded_Files =
       syntax.load_command(name) match {
         case None => Loaded_Files.none
         case Some(a) =>
           load_commands.find(_.name == a) match {
             case Some(load_command) => load_command.loaded_files(clean_arguments)
             case None => error("Undefined load command function: " + a)
           }
       }
   }
 
   val empty: Span = Span(Ignored_Span, Nil)
 
   def unparsed(source: String, theory: Boolean): Span =
   {
     val kind = if (theory) Theory_Span else Malformed_Span
     Span(kind, List(Token(Token.Kind.UNPARSED, source)))
   }
 }