diff -r 9bf36baa8686 -r a8e5d7c9a834 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Sat Jan 09 15:56:09 2021 +0100
+++ b/src/Pure/PIDE/command_span.scala	Sat Jan 09 18:56:53 2021 +0100
@@ -47,13 +47,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, abs_pos: Position.T) extends Kind
+  case class Command_Span(name: String, pos: Position.T) extends Kind
   case object Ignored_Span extends Kind
   case object Malformed_Span extends Kind
   case object Theory_Span extends Kind
@@ -71,9 +71,6 @@
     def position: Position.T =
       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 =>