# HG changeset patch
# User wenzelm
# Date 1606852039 -3600
# Node ID 51683cd9d7fa7c71c88e6131afdae3034fe898f8
# Parent  e732c98b02e63da6c0185792ecaa570234e5e848# Parent  85bcdd05c6d0168d690f5aa023bb78b056e3f9b0
merged

diff -r e732c98b02e6 -r 51683cd9d7fa src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Dec 01 15:29:54 2020 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Dec 01 20:47:19 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()
diff -r e732c98b02e6 -r 51683cd9d7fa src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Tue Dec 01 15:29:54 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala	Tue Dec 01 20:47:19 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 {
diff -r e732c98b02e6 -r 51683cd9d7fa src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Dec 01 15:29:54 2020 +0100
+++ b/src/Pure/PIDE/headless.scala	Tue Dec 01 20:47:19 2020 +0100
@@ -256,7 +256,7 @@
       val dep_theories = dependencies.theories
       val dep_theories_set = dep_theories.toSet
       val dep_files =
-        dependencies.loaded_files(false).flatMap(_._2).
+        dependencies.loaded_files.flatMap(_._2).
           map(path => Document.Node.Name(resources.append("", path)))
 
       val use_theories_state =
diff -r e732c98b02e6 -r 51683cd9d7fa src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Dec 01 15:29:54 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Dec 01 20:47:19 2020 +0100
@@ -398,20 +398,17 @@
         graph2.map_node(name, _ => syntax)
       })
 
-    def loaded_files(pure: Boolean): List[(String, List[Path])] =
+    def loaded_files: List[(String, List[Path])] =
     {
-      val loaded_files =
-        theories.map(_.theory) zip
-          Par_List.map((e: () => List[Path]) => e(),
-            theories.map(name =>
-              resources.loaded_files(loaded_theories.get_node(name.theory), name)))
-
-      if (pure) {
-        val pure_files = resources.pure_files(overall_syntax)
-        loaded_files.map({ case (name, files) =>
-          (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
-      }
-      else loaded_files
+      theories.zip(
+        Par_List.map((e: () => List[Path]) => e(),
+          theories.map(name =>
+            resources.loaded_files(loaded_theories.get_node(name.theory), name))))
+        .map({ case (name, files) =>
+          val files1 =
+            if (name.theory == Thy_Header.PURE) resources.pure_files(overall_syntax) ::: files
+            else files
+          (name.theory, files1) })
     }
 
     def imported_files: List[Path] =
diff -r e732c98b02e6 -r 51683cd9d7fa src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Dec 01 15:29:54 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Dec 01 20:47:19 2020 +0100
@@ -173,10 +173,7 @@
             val theory_files = dependencies.theories.map(_.path)
 
             val (loaded_files, loaded_files_errors) =
-              try {
-                if (inlined_files) (dependencies.loaded_files(Sessions.is_pure(info.name)), Nil)
-                else (Nil, Nil)
-              }
+              try { if (inlined_files) (dependencies.loaded_files, Nil) else (Nil, Nil) }
               catch { case ERROR(msg) => (Nil, List(msg)) }
 
             val session_files =