clarified signature --- more positions;

--- a/src/Pure/Isar/outer_syntax.scala	Tue Dec 01 16:07:19 2020 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Dec 01 20:47:03 2020 +0100
@@ -165,25 +165,29 @@
     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()

--- a/src/Pure/PIDE/command_span.scala	Tue Dec 01 16:07:19 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala	Tue Dec 01 20:47:03 2020 +0100
@@ -46,13 +46,13 @@
   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
@@ -65,10 +65,13 @@
     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 {