# HG changeset patch
# User wenzelm
# Date 1610215013 -3600
# Node ID a8e5d7c9a83408fd87e8b0b4a96c7a0f747b0d07
# Parent  9bf36baa8686edc86fbfff4cb51b890ecb67df86
discontinued odd absolute position (amending 85bcdd05c6d0, 1975f397eabb): it violates translation invariance of commands and may lead to redundant re-checking of PIDE document;

diff -r 9bf36baa8686 -r a8e5d7c9a834 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Sat Jan 09 15:56:09 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Sat Jan 09 18:56:53 2021 +0100
@@ -165,7 +165,6 @@
     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])
     {
@@ -182,11 +181,8 @@
                   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)
     }
 
diff -r 9bf36baa8686 -r a8e5d7c9a834 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Jan 09 15:56:09 2021 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Jan 09 18:56:53 2021 +0100
@@ -614,7 +614,7 @@
           val opt_range =
             reported_range orElse {
               if (name == Symbol.Text_Chunk.Default)
-                Position.Range.unapply(span.absolute_position)
+                Position.Range.unapply(span.position)
               else None
             }
           opt_range match {
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 =>