src/Pure/PIDE/command_span.scala

--- 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 {