# HG changeset patch
# User wenzelm
# Date 1607193037 -3600
# Node ID 18bc50e58e38c4dac45c83de6dc89acf2ebac424
# Parent  b09f358f3eb0b94ba1d19824d70697d86b0db4cb# Parent  1975f397eabbf8ee57f7faac658192bc3a10f7f8
merged

diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/Isar/document_structure.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -101,7 +101,7 @@
     /* result structure */
 
     val spans = syntax.parse_spans(text)
-    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
+    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.Blobs_Info.none, span)))
     result()
   }
 
@@ -174,7 +174,7 @@
     for { span <- syntax.parse_spans(text) } {
       sections.add(
         new Command_Item(syntax.keywords,
-          Command(Document_ID.none, node_name, Command.no_blobs, span)))
+          Command(Document_ID.none, node_name, Command.Blobs_Info.none, span)))
     }
     sections.result()
   }
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/ML/ml_compiler.ML	Sat Dec 05 19:30:37 2020 +0100
@@ -117,7 +117,8 @@
       |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
       |> Output.report;
     val _ =
-      if not (null persistent_reports) andalso redirect andalso Future.enabled ()
+      if not (null persistent_reports) andalso redirect andalso
+        not (Options.default_bool "build_pide_reports") andalso Future.enabled ()
       then
         Execution.print
           {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/PIDE/command.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -8,21 +8,44 @@
 package isabelle
 
 
-import scala.collection.mutable
 import scala.collection.immutable.SortedMap
 
 
 object Command
 {
-  type Edit = (Option[Command], Option[Command])
+  /* blobs */
+
+  object Blob
+  {
+    def read_file(name: Document.Node.Name, src_path: Path): Blob =
+    {
+      val bytes = Bytes.read(name.path)
+      val chunk = Symbol.Text_Chunk(bytes.text)
+      Blob(name, src_path, Some((bytes.sha1_digest, chunk)))
+    }
+  }
 
   sealed case class Blob(
     name: Document.Node.Name,
     src_path: Path,
     content: Option[(SHA1.Digest, Symbol.Text_Chunk)])
+  {
+    def read_file: String = File.read(name.path)
 
-  type Blobs_Info = (List[Exn.Result[Blob]], Int)
-  val no_blobs: Blobs_Info = (Nil, -1)
+    def chunk_file: Symbol.Text_Chunk.File =
+      Symbol.Text_Chunk.File(name.node)
+  }
+
+  object Blobs_Info
+  {
+    val none: Blobs_Info = Blobs_Info(Nil, -1)
+
+    def errors(msgs: List[String]): Blobs_Info =
+      Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg))), -1)
+  }
+
+  sealed case class Blobs_Info(blobs: List[Exn.Result[Blob]], index: Int)
+
 
 
   /** accumulated results from prover **/
@@ -101,6 +124,7 @@
   object Markup_Index
   {
     val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default)
+    def blob(blob: Blob): Markup_Index = Markup_Index(false, blob.chunk_file)
   }
 
   sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name)
@@ -287,10 +311,9 @@
               def bad(): Unit = Output.warning("Ignored report message: " + msg)
 
               msg match {
-                case XML.Elem(Markup(name, atts1), args) =>
-                  val atts = atts1 ::: atts0
-                  command.reported_position(atts) match {
-                    case Some((id, chunk_name)) =>
+                case XML.Elem(Markup(name, atts), args) =>
+                  command.reported_position(atts) orElse command.reported_position(atts0) match {
+                    case Some((id, chunk_name, target_range)) =>
                       val target =
                         if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
                           Some((chunk_name, command.chunks(chunk_name)))
@@ -298,8 +321,8 @@
                           other_id(command.node_name, id)
                         else None
 
-                      (target, atts) match {
-                        case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
+                      (target, target_range) match {
+                        case (Some((target_name, target_chunk)), Some(symbol_range)) =>
                           target_chunk.incorporate(symbol_range) match {
                             case Some(range) =>
                               val props = atts.filterNot(Markup.position_property)
@@ -359,18 +382,19 @@
   }
 
   val empty: Command =
-    Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty)
+    Command(Document_ID.none, Document.Node.Name.empty, Blobs_Info.none, Command_Span.empty)
 
   def unparsed(
     source: String,
     theory: Boolean = false,
     id: Document_ID.Command = Document_ID.none,
     node_name: Document.Node.Name = Document.Node.Name.empty,
+    blobs_info: Blobs_Info = Blobs_Info.none,
     results: Results = Results.empty,
     markups: Markups = Markups.empty): Command =
   {
     val (source1, span1) = Command_Span.unparsed(source, theory).compact_source
-    new Command(id, node_name, no_blobs, span1, source1, results, markups)
+    new Command(id, node_name, blobs_info, span1, source1, results, markups)
   }
 
   def text(source: String): Command = unparsed(source)
@@ -380,7 +404,9 @@
       markups = Markups.init(Markup_Tree.from_XML(body)))
 
 
-  /* perspective */
+  /* edits and perspective */
+
+  type Edit = (Option[Command], Option[Command])
 
   object Perspective
   {
@@ -431,13 +457,11 @@
           yield {
             val completion =
               if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
-            val msg =
-              "Bad theory import " +
-                Markup.Path(import_name.node).markup(quote(import_name.toString)) +
-                Position.here(pos) + Completion.report_theories(pos, completion)
-            Exn.Exn[Command.Blob](ERROR(msg))
+            "Bad theory import " +
+              Markup.Path(import_name.node).markup(quote(import_name.toString)) +
+              Position.here(pos) + Completion.report_theories(pos, completion)
           }
-        (errors, -1)
+        Blobs_Info.errors(errors)
 
       // auxiliary files
       case _ =>
@@ -450,9 +474,29 @@
               val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
               Blob(name, src_path, content)
             }).user_error)
-        (blobs, loaded_files.index)
+        Blobs_Info(blobs, loaded_files.index)
     }
   }
+
+  def build_blobs_info(
+    syntax: Outer_Syntax,
+    node_name: Document.Node.Name,
+    load_commands: List[Command_Span.Span]): Blobs_Info =
+  {
+    val blobs =
+      for {
+        span <- load_commands
+        file <- span.loaded_files(syntax).files
+      } yield {
+        (Exn.capture {
+          val dir = node_name.master_dir_path
+          val src_path = Path.explode(file)
+          val name = Document.Node.Name((dir + src_path).expand.implode_symbolic)
+          Blob.read_file(name, src_path)
+        }).user_error
+      }
+    Blobs_Info(blobs, -1)
+  }
 }
 
 
@@ -482,8 +526,8 @@
 
   /* blobs */
 
-  def blobs: List[Exn.Result[Command.Blob]] = blobs_info._1
-  def blobs_index: Int = blobs_info._2
+  def blobs: List[Exn.Result[Command.Blob]] = blobs_info.blobs
+  def blobs_index: Int = blobs_info.index
 
   def blobs_ok: Boolean =
     blobs.forall({ case Exn.Res(_) => true case _ => false })
@@ -508,7 +552,7 @@
   val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
     ((Symbol.Text_Chunk.Default -> chunk) ::
       (for (Exn.Res(blob) <- blobs; (_, file) <- blob.content)
-        yield Symbol.Text_Chunk.File(blob.name.node) -> file)).toMap
+        yield blob.chunk_file -> file)).toMap
 
   def length: Int = source.length
   def range: Text.Range = chunk.range
@@ -522,7 +566,9 @@
 
   /* reported positions */
 
-  def reported_position(pos: Position.T): Option[(Document_ID.Generic, Symbol.Text_Chunk.Name)] =
+  def reported_position(pos: Position.T)
+    : Option[(Document_ID.Generic, Symbol.Text_Chunk.Name, Option[Symbol.Range])] =
+  {
     pos match {
       case Position.Id(id) =>
         val chunk_name =
@@ -531,9 +577,10 @@
               Symbol.Text_Chunk.File(name)
             case _ => Symbol.Text_Chunk.Default
           }
-        Some((id, chunk_name))
+        Some((id, chunk_name, Position.Range.unapply(pos)))
       case _ => None
     }
+  }
 
   def message_positions(
     self_id: Document_ID.Generic => Boolean,
@@ -543,11 +590,11 @@
   {
     def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       reported_position(props) match {
-        case Some((id, name)) if self_id(id) && name == chunk_name =>
+        case Some((id, name, reported_range)) if self_id(id) && name == chunk_name =>
           val opt_range =
-            Position.Range.unapply(props) orElse {
+            reported_range orElse {
               if (name == Symbol.Text_Chunk.Default)
-                Position.Range.unapply(span.position)
+                Position.Range.unapply(span.absolute_position)
               else None
             }
           opt_range match {
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/PIDE/command_span.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -122,6 +122,9 @@
       else Nil
     }
 
+    def is_load_command(syntax: Outer_Syntax): Boolean =
+      syntax.load_command(name).isDefined
+
     def loaded_files(syntax: Outer_Syntax): Loaded_Files =
       syntax.load_command(name) match {
         case None => Loaded_Files.none
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/PIDE/document.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -128,6 +128,11 @@
       def path: Path = Path.explode(File.standard_path(node))
       def master_dir_path: Path = Path.explode(File.standard_path(master_dir))
 
+      def expand: Name =
+        Name(path.expand.implode, master_dir_path.expand.implode, theory)
+      def symbolic: Name =
+        Name(path.implode_symbolic, master_dir_path.implode_symbolic, theory)
+
       def is_theory: Boolean = theory.nonEmpty
 
       def theory_base_name: String = Long_Name.base_name(theory)
@@ -526,31 +531,66 @@
   }
 
 
-  /* snapshot */
+  /* snapshot: persistent user-view of document state */
 
   object Snapshot
   {
     val init: Snapshot = State.init.snapshot()
   }
 
-  abstract class Snapshot
+  class Snapshot private[Document](
+    val state: State,
+    val version: Version,
+    val node_name: Node.Name,
+    edits: List[Text.Edit],
+    snippet_command: Option[Command])
   {
-    def state: State
-    def version: Version
-    def is_outdated: Boolean
+    override def toString: String =
+      "Snapshot(node = " + node_name.node + ", version = " + version.id +
+        (if (is_outdated) ", outdated" else "") + ")"
+
+
+    /* nodes */
+
+    def get_node(name: Node.Name): Node = version.nodes(name)
+
+    val node: Node = get_node(node_name)
+
+    def node_files: List[Node.Name] =
+      node_name :: (node.load_commands ::: snippet_command.toList).flatMap(_.blobs_names)
+
+
+    /* edits */
+
+    def is_outdated: Boolean = edits.nonEmpty
 
-    def convert(i: Text.Offset): Text.Offset
-    def revert(i: Text.Offset): Text.Offset
-    def convert(range: Text.Range): Text.Range
-    def revert(range: Text.Range): Text.Range
+    private lazy val reverse_edits = edits.reverse
+
+    def convert(offset: Text.Offset): Text.Offset =
+      (offset /: edits)((i, edit) => edit.convert(i))
+    def revert(offset: Text.Offset): Text.Offset =
+      (offset /: reverse_edits)((i, edit) => edit.revert(i))
+
+    def convert(range: Text.Range): Text.Range = range.map(convert)
+    def revert(range: Text.Range): Text.Range = range.map(revert)
+
+
+    /* theory load commands */
 
-    def node_name: Node.Name
-    def node: Node
-    def nodes: List[(Node.Name, Node)]
+    val commands_loading: List[Command] =
+      if (node_name.is_theory) Nil
+      else version.nodes.commands_loading(node_name)
 
-    def commands_loading: List[Command]
-    def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
-    def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
+    def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] =
+      (for {
+        cmd <- node.load_commands.iterator
+        blob_name <- cmd.blobs_names.iterator
+        if pred(blob_name)
+        start <- node.command_start(cmd)
+      } yield convert(cmd.core_range + start)).toList
+
+
+    /* command as add-on snippet */
 
     def command_snippet(command: Command): Snapshot =
     {
@@ -569,37 +609,156 @@
           .define_version(version1, state0.the_assignment(version))
           .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
 
-      state1.snapshot(name = node_name)
+      state1.snapshot(node_name = node_name, snippet_command = Some(command))
     }
 
+
+    /* XML markup */
+
     def xml_markup(
-      range: Text.Range = Text.Range.full,
-      elements: Markup.Elements = Markup.Elements.full): XML.Body
-    def messages: List[(XML.Tree, Position.T)]
-    def exports: List[Export.Entry]
-    def exports_map: Map[String, Export.Entry]
+        range: Text.Range = Text.Range.full,
+        elements: Markup.Elements = Markup.Elements.full): XML.Body =
+      state.xml_markup(version, node_name, range = range, elements = elements)
+
+    def xml_markup_blobs(elements: Markup.Elements = Markup.Elements.full): List[XML.Body] =
+    {
+      snippet_command match {
+        case None => Nil
+        case Some(command) =>
+          for (Exn.Res(blob) <- command.blobs)
+          yield {
+            val text = blob.read_file
+            val markup = command.init_markups(Command.Markup_Index.blob(blob))
+            markup.to_XML(Text.Range(0, text.length), text, elements)
+          }
+      }
+    }
+
+
+    /* messages */
+
+    lazy val messages: List[(XML.Tree, Position.T)] =
+      (for {
+        (command, start) <-
+          Document.Node.Commands.starts_pos(
+            node.commands.iterator, Token.Pos.file(node_name.node))
+        pos = command.span.keyword_pos(start).position(command.span.name)
+        (_, tree) <- state.command_results(version, command).iterator
+       } yield (tree, pos)).toList
+
+
+    /* exports */
+
+    lazy val exports: List[Export.Entry] =
+      state.node_exports(version, node_name).iterator.map(_._2).toList
+
+    lazy val exports_map: Map[String, Export.Entry] =
+      (for (entry <- exports.iterator) yield (entry.name, entry)).toMap
+
+
+    /* find command */
 
-    def find_command(id: Document_ID.Generic): Option[(Node, Command)]
+    def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
+      state.lookup_id(id) match {
+        case None => None
+        case Some(st) =>
+          val command = st.command
+          val command_node = get_node(command.node_name)
+          if (command_node.commands.contains(command)) Some((command_node, command)) else None
+      }
+
     def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
-      : Option[Line.Node_Position]
+        : Option[Line.Node_Position] =
+      for ((node, command) <- find_command(id))
+      yield {
+        val name = command.node_name.node
+        val sources_iterator =
+          node.commands.iterator.takeWhile(_ != command).map(_.source) ++
+            (if (offset == 0) Iterator.empty
+             else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
+        val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+        Line.Node_Position(name, pos)
+      }
+
+    def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
+      if (other_node_name.is_theory) {
+        val other_node = get_node(other_node_name)
+        val iterator = other_node.command_iterator(revert(offset) max 0)
+        if (iterator.hasNext) {
+          val (command0, _) = iterator.next
+          other_node.commands.reverse.iterator(command0).find(command => !command.is_ignored)
+        }
+        else other_node.commands.reverse.iterator.find(command => !command.is_ignored)
+      }
+      else version.nodes.commands_loading(other_node_name).headOption
+
+
+    /* command results */
+
+    def command_results(range: Text.Range): Command.Results =
+      Command.State.merge_results(
+        select[List[Command.State]](range, Markup.Elements.full, command_states =>
+          { case _ => Some(command_states) }).flatMap(_.info))
+
+    def command_results(command: Command): Command.Results =
+      state.command_results(version, command)
+
+
+    /* command ids: static and dynamic */
+
+    def command_id_map: Map[Document_ID.Generic, Command] =
+      state.command_id_map(version, get_node(node_name).commands)
+
+
+    /* cumulate markup */
 
     def cumulate[A](
       range: Text.Range,
       info: A,
       elements: Markup.Elements,
       result: List[Command.State] => (A, Text.Markup) => Option[A],
-      status: Boolean = false): List[Text.Info[A]]
+      status: Boolean = false): List[Text.Info[A]] =
+    {
+      val former_range = revert(range).inflate_singularity
+      val (chunk_name, command_iterator) =
+        commands_loading.headOption match {
+          case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
+          case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
+        }
+      val markup_index = Command.Markup_Index(status, chunk_name)
+      (for {
+        (command, command_start) <- command_iterator
+        chunk <- command.chunks.get(chunk_name).iterator
+        states = state.command_states(version, command)
+        res = result(states)
+        markup_range <- (former_range - command_start).try_restrict(chunk.range).iterator
+        markup = Command.State.merge_markup(states, markup_index, markup_range, elements)
+        Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements,
+          {
+            case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
+          }).iterator
+        r1 <- convert(r0 + command_start).try_restrict(range).iterator
+      } yield Text.Info(r1, a)).toList
+    }
 
     def select[A](
       range: Text.Range,
       elements: Markup.Elements,
       result: List[Command.State] => Text.Markup => Option[A],
-      status: Boolean = false): List[Text.Info[A]]
-
-    def command_results(range: Text.Range): Command.Results
-    def command_results(command: Command): Command.Results
-
-    def command_id_map: Map[Document_ID.Generic, Command]
+      status: Boolean = false): List[Text.Info[A]] =
+    {
+      def result1(states: List[Command.State]): (Option[A], Text.Markup) => Option[Option[A]] =
+      {
+        val res = result(states)
+        (_: Option[A], x: Text.Markup) =>
+          res(x) match {
+            case None => None
+            case some => Some(some)
+          }
+      }
+      for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
+        yield Text.Info(r, x)
+    }
   }
 
 
@@ -814,12 +973,20 @@
           st <- command_states(version, command).iterator
         } yield st.exports)
 
-    def begin_theory(node_name: Node.Name, id: Document_ID.Exec, source: String): State =
+    def begin_theory(
+      node_name: Node.Name,
+      id: Document_ID.Exec,
+      source: String,
+      blobs_info: Command.Blobs_Info): State =
+    {
       if (theories.isDefinedAt(id)) fail
       else {
-        val command = Command.unparsed(source, theory = true, id = id, node_name = node_name)
+        val command =
+          Command.unparsed(source, theory = true, id = id, node_name = node_name,
+            blobs_info = blobs_info)
         copy(theories = theories + (id -> command.empty_state))
       }
+    }
 
     def end_theory(theory: String): (Snapshot, State) =
       theories.collectFirst({ case (_, st) if st.command.node_name.theory == theory => st }) match {
@@ -829,9 +996,9 @@
           val node_name = command.node_name
           val command1 =
             Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name,
-              results = st.results, markups = st.markups)
+              blobs_info = command.blobs_info, results = st.results, markups = st.markups)
           val state1 = copy(theories = theories - command1.id)
-          val snapshot = state1.snapshot(name = node_name).command_snippet(command1)
+          val snapshot = state1.snapshot(node_name = node_name).command_snippet(command1)
           (snapshot, state1)
       }
 
@@ -1061,21 +1228,21 @@
         it.hasNext && command_states(version, it.next).exists(_.consolidated)
       }
 
-    // persistent user-view
-    def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
-      : Snapshot =
+    def snapshot(
+      node_name: Node.Name = Node.Name.empty,
+      pending_edits: List[Text.Edit] = Nil,
+      snippet_command: Option[Command] = None): Snapshot =
     {
+      /* pending edits and unstable changes */
+
       val stable = recent_stable
-      val latest = history.tip
-
-
-      /* pending edits and unstable changes */
+      val version = stable.version.get_finished
 
       val rev_pending_changes =
         for {
           change <- history.undo_list.takeWhile(_ != stable)
-          (a, edits) <- change.rev_edits
-          if a == name
+          (name, edits) <- change.rev_edits
+          if name == node_name
         } yield edits
 
       val edits =
@@ -1083,176 +1250,8 @@
           case (edits, Node.Edits(es)) => es ::: edits
           case (edits, _) => edits
         })
-      lazy val reverse_edits = edits.reverse
 
-      new Snapshot
-      {
-        /* global information */
-
-        val state: State = State.this
-        val version: Version = stable.version.get_finished
-        val is_outdated: Boolean = pending_edits.nonEmpty || latest != stable
-
-
-        /* local node content */
-
-        def convert(offset: Text.Offset): Text.Offset = (offset /: edits)((i, edit) => edit.convert(i))
-        def revert(offset: Text.Offset): Text.Offset = (offset /: reverse_edits)((i, edit) => edit.revert(i))
-
-        def convert(range: Text.Range): Text.Range = range.map(convert)
-        def revert(range: Text.Range): Text.Range = range.map(revert)
-
-        val node_name: Node.Name = name
-        val node: Node = version.nodes(name)
-
-        def nodes: List[(Node.Name, Node)] =
-          (node_name :: node.load_commands.flatMap(_.blobs_names)).
-            map(name => (name, version.nodes(name)))
-
-        val commands_loading: List[Command] =
-          if (node_name.is_theory) Nil
-          else version.nodes.commands_loading(node_name)
-
-        def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] =
-          (for {
-            cmd <- node.load_commands.iterator
-            blob_name <- cmd.blobs_names.iterator
-            if pred(blob_name)
-            start <- node.command_start(cmd)
-          } yield convert(cmd.core_range + start)).toList
-
-        def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
-          if (other_node_name.is_theory) {
-            val other_node = version.nodes(other_node_name)
-            val iterator = other_node.command_iterator(revert(offset) max 0)
-            if (iterator.hasNext) {
-              val (command0, _) = iterator.next
-              other_node.commands.reverse.iterator(command0).find(command => !command.is_ignored)
-            }
-            else other_node.commands.reverse.iterator.find(command => !command.is_ignored)
-          }
-          else version.nodes.commands_loading(other_node_name).headOption
-
-        def xml_markup(
-            range: Text.Range = Text.Range.full,
-            elements: Markup.Elements = Markup.Elements.full): XML.Body =
-          state.xml_markup(version, node_name, range = range, elements = elements)
-
-        lazy val messages: List[(XML.Tree, Position.T)] =
-          (for {
-            (command, start) <-
-              Document.Node.Commands.starts_pos(
-                node.commands.iterator, Token.Pos.file(node_name.node))
-            pos = command.span.keyword_pos(start).position(command.span.name)
-            (_, tree) <- state.command_results(version, command).iterator
-           } yield (tree, pos)).toList
-
-        lazy val exports: List[Export.Entry] =
-          state.node_exports(version, node_name).iterator.map(_._2).toList
-
-        lazy val exports_map: Map[String, Export.Entry] =
-          (for (entry <- exports.iterator) yield (entry.name, entry)).toMap
-
-
-        /* find command */
-
-        def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
-          state.lookup_id(id) match {
-            case None => None
-            case Some(st) =>
-              val command = st.command
-              val node = version.nodes(command.node_name)
-              if (node.commands.contains(command)) Some((node, command)) else None
-          }
-
-        def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
-            : Option[Line.Node_Position] =
-          for ((node, command) <- find_command(id))
-          yield {
-            val name = command.node_name.node
-            val sources_iterator =
-              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
-                (if (offset == 0) Iterator.empty
-                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
-            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
-            Line.Node_Position(name, pos)
-          }
-
-
-        /* cumulate markup */
-
-        def cumulate[A](
-          range: Text.Range,
-          info: A,
-          elements: Markup.Elements,
-          result: List[Command.State] => (A, Text.Markup) => Option[A],
-          status: Boolean = false): List[Text.Info[A]] =
-        {
-          val former_range = revert(range).inflate_singularity
-          val (chunk_name, command_iterator) =
-            commands_loading.headOption match {
-              case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
-              case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
-            }
-          val markup_index = Command.Markup_Index(status, chunk_name)
-          (for {
-            (command, command_start) <- command_iterator
-            chunk <- command.chunks.get(chunk_name).iterator
-            states = state.command_states(version, command)
-            res = result(states)
-            markup_range <- (former_range - command_start).try_restrict(chunk.range).iterator
-            markup = Command.State.merge_markup(states, markup_index, markup_range, elements)
-            Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements,
-              {
-                case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
-              }).iterator
-            r1 <- convert(r0 + command_start).try_restrict(range).iterator
-          } yield Text.Info(r1, a)).toList
-        }
-
-        def select[A](
-          range: Text.Range,
-          elements: Markup.Elements,
-          result: List[Command.State] => Text.Markup => Option[A],
-          status: Boolean = false): List[Text.Info[A]] =
-        {
-          def result1(states: List[Command.State]): (Option[A], Text.Markup) => Option[Option[A]] =
-          {
-            val res = result(states)
-            (_: Option[A], x: Text.Markup) =>
-              res(x) match {
-                case None => None
-                case some => Some(some)
-              }
-          }
-          for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
-            yield Text.Info(r, x)
-        }
-
-
-        /* command results */
-
-        def command_results(range: Text.Range): Command.Results =
-          Command.State.merge_results(
-            select[List[Command.State]](range, Markup.Elements.full, command_states =>
-              { case _ => Some(command_states) }).flatMap(_.info))
-
-        def command_results(command: Command): Command.Results =
-          state.command_results(version, command)
-
-
-        /* command ids: static and dynamic */
-
-        def command_id_map: Map[Document_ID.Generic, Command] =
-          state.command_id_map(version, version.nodes(node_name).commands)
-
-
-        /* output */
-
-        override def toString: String =
-          "Snapshot(node = " + node_name.node + ", version = " + version.id +
-            (if (is_outdated) ", outdated" else "") + ")"
-      }
+      new Snapshot(this, version, node_name, edits, snippet_command)
     }
   }
 }
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/PIDE/headless.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -256,8 +256,8 @@
       val dep_theories = dependencies.theories
       val dep_theories_set = dep_theories.toSet
       val dep_files =
-        dependencies.loaded_files.flatMap(_._2).
-          map(path => Document.Node.Name(resources.append("", path)))
+        for (path <- dependencies.loaded_files)
+          yield Document.Node.Name(resources.append("", path))
 
       val use_theories_state =
       {
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -58,7 +58,7 @@
       var result: List[XML.Elem] = Nil
       for (elem <- rev_markup if elements(elem.name))
         result ::= elem
-      result.toList
+      result
     }
 
     def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/PIDE/query_operation.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -84,7 +84,7 @@
               (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
               if props.contains((Markup.INSTANCE, state0.instance))
             } yield elem).toList
-          val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
+          val removed = !snapshot.get_node(cmd.node_name).commands.contains(cmd)
           (snapshot, command_results, results, removed)
         case None =>
           (Document.Snapshot.init, Command.Results.empty, Nil, true)
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/PIDE/resources.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -106,36 +106,38 @@
 
   /* theory files */
 
-  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] =
+  def load_commands(syntax: Outer_Syntax, name: Document.Node.Name)
+    : () => List[Command_Span.Span] =
   {
     val (is_utf8, raw_text) =
       with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString))
-    () => {
-      if (syntax.has_load_commands(raw_text)) {
-        val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text))
-        val spans = syntax.parse_spans(text)
-        val dir = Path.explode(name.master_dir)
-        (for {
-          span <- spans.iterator
-          file <- span.loaded_files(syntax).files
-        } yield (dir + Path.explode(file)).expand).toList
+    () =>
+      {
+        if (syntax.has_load_commands(raw_text)) {
+          val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text))
+          syntax.parse_spans(text).filter(_.is_load_command(syntax))
+        }
+        else Nil
       }
-      else Nil
-    }
+  }
+
+  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name, spans: List[Command_Span.Span])
+    : List[Path] =
+  {
+    val dir = name.master_dir_path
+    for { span <- spans; file <- span.loaded_files(syntax).files }
+      yield (dir + Path.explode(file)).expand
   }
 
   def pure_files(syntax: Outer_Syntax): List[Path] =
   {
     val pure_dir = Path.explode("~~/src/Pure")
-    val roots =
-      for { (name, _) <- Thy_Header.ml_roots }
-      yield (pure_dir + Path.explode(name)).expand
-    val files =
-      for {
-        (path, (_, theory)) <- roots zip Thy_Header.ml_roots
-        file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
-      } yield file
-    roots ::: files
+    for {
+      (name, theory) <- Thy_Header.ml_roots
+      path = (pure_dir + Path.explode(name)).expand
+      node_name = Document.Node.Name(path.implode, path.dir.implode, theory)
+      file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)())
+    } yield file
   }
 
   def theory_name(qualifier: String, theory: String): String =
@@ -398,19 +400,31 @@
         graph2.map_node(name, _ => syntax)
       })
 
-    def loaded_files: List[(String, List[Path])] =
-    {
+    def get_syntax(name: Document.Node.Name): Outer_Syntax =
+      loaded_theories.get_node(name.theory)
+
+    def load_commands: List[(Document.Node.Name, List[Command_Span.Span])] =
       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) })
+        Par_List.map((e: () => List[Command_Span.Span]) => e(),
+          theories.map(name => resources.load_commands(get_syntax(name), name))))
+      .filter(p => p._2.nonEmpty)
+
+    def loaded_files(name: Document.Node.Name, spans: List[Command_Span.Span])
+      : (String, List[Path]) =
+    {
+      val theory = name.theory
+      val syntax = get_syntax(name)
+      val files1 = resources.loaded_files(syntax, name, spans)
+      val files2 = if (theory == Thy_Header.PURE) pure_files(syntax) else Nil
+      (theory, files1 ::: files2)
     }
 
+    def loaded_files: List[Path] =
+      for {
+        (name, spans) <- load_commands
+        file <- loaded_files(name, spans)._2
+      } yield file
+
     def imported_files: List[Path] =
     {
       val base_theories =
@@ -418,7 +432,7 @@
           filter(session_base.loaded_theories.defined)
 
       base_theories.map(theory => session_base.known_theories(theory).name.path) :::
-      base_theories.flatMap(session_base.known_loaded_files(_))
+      base_theories.flatMap(session_base.known_loaded_files.withDefaultValue(Nil))
     }
 
     lazy val overall_syntax: Outer_Syntax =
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/PIDE/session.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -130,6 +130,9 @@
   val xml_cache: XML.Cache = XML.make_cache()
   val xz_cache: XZ.Cache = XZ.make_cache()
 
+  def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
+    Command.Blobs_Info.none
+
 
   /* global flags */
 
@@ -506,7 +509,8 @@
                 change_command(_.add_export(id, (args.serial, export)))
 
               case Protocol.Loading_Theory(node_name, id) =>
-                try { global_state.change(_.begin_theory(node_name, id, msg.text)) }
+                val blobs_info = build_blobs_info(node_name)
+                try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) }
                 catch { case _: Document.State.Fail => bad_output() }
 
               case Markup.Finished_Theory(theory) =>
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/Pure.thy	Sat Dec 05 19:30:37 2020 +0100
@@ -168,6 +168,9 @@
 
 in end\<close>
 
+external_file "ROOT0.ML"
+external_file "ROOT.ML"
+
 
 subsection \<open>Embedded ML text\<close>
 
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/Thy/export.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -16,6 +16,7 @@
   /* artefact names */
 
   val MARKUP = "PIDE/markup"
+  val FILES = "PIDE/files"
   val MESSAGES = "PIDE/messages"
   val DOCUMENT_PREFIX = "document/"
   val CITATIONS = DOCUMENT_PREFIX + "citations"
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/Thy/sessions.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -55,6 +55,7 @@
     document_theories: List[Document.Node.Name] = Nil,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[(Document.Node.Name, Options)] = Nil,
+    load_commands: Map[Document.Node.Name, List[Command_Span.Span]] = Map.empty,
     known_theories: Map[String, Document.Node.Entry] = Map.empty,
     known_loaded_files: Map[String, List[Path]] = Map.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -172,10 +173,15 @@
 
             val theory_files = dependencies.theories.map(_.path)
 
-            val (loaded_files, loaded_files_errors) =
-              try { if (inlined_files) (dependencies.loaded_files, Nil) else (Nil, Nil) }
+            dependencies.load_commands
+
+            val (load_commands, load_commands_errors) =
+              try { if (inlined_files) (dependencies.load_commands, Nil) else (Nil, Nil) }
               catch { case ERROR(msg) => (Nil, List(msg)) }
 
+            val loaded_files =
+              load_commands.map({ case (name, spans) => dependencies.loaded_files(name, spans) })
+
             val session_files =
               (theory_files ::: loaded_files.flatMap(_._2) :::
                 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
@@ -325,13 +331,14 @@
                 document_theories = document_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = dependencies.theories_adjunct,
+                load_commands = load_commands.toMap,
                 known_theories = known_theories,
                 known_loaded_files = known_loaded_files,
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),
                 sources = check_sources(session_files),
                 session_graph_display = session_graph_display,
-                errors = dependencies.errors ::: loaded_files_errors ::: import_errors :::
+                errors = dependencies.errors ::: load_commands_errors ::: import_errors :::
                   document_errors ::: dir_errors ::: sources_errors ::: path_errors :::
                   bibtex_errors)
 
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/Tools/build_job.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -28,6 +28,7 @@
     Future.thread("build", uninterruptible = true) {
       val parent = info.parent.getOrElse("")
       val base = deps(parent)
+      val result_base = deps(session_name)
 
       val env =
         Isabelle_System.settings() +
@@ -50,6 +51,16 @@
         new Session(options, resources) {
           override val xml_cache: XML.Cache = store.xml_cache
           override val xz_cache: XZ.Cache = store.xz_cache
+
+          override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
+          {
+            result_base.load_commands.get(name.expand) match {
+              case Some(spans) =>
+                val syntax = result_base.theory_syntax(name)
+                Command.build_blobs_info(syntax, name, spans)
+              case None => Command.Blobs_Info.none
+            }
+          }
         }
       def make_rendering(snapshot: Document.Snapshot): Rendering =
         new Rendering(snapshot, options, session) {
@@ -176,6 +187,11 @@
             def export_text(name: String, text: String): Unit =
               export(name, List(XML.Text(text)))
 
+            export_text(Export.FILES, cat_lines(snapshot.node_files.map(_.symbolic.node)))
+
+            for ((xml, i) <- snapshot.xml_markup_blobs().zipWithIndex) {
+              export(Export.MARKUP + (i + 1), xml)
+            }
             export(Export.MARKUP, snapshot.xml_markup())
             export(Export.MESSAGES, snapshot.messages.map(_._1))
 
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Pure/Tools/update.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -43,7 +43,8 @@
         progress.echo("Processing theory " + args.print_node + " ...")
 
         val snapshot = args.snapshot
-        for ((node_name, node) <- snapshot.nodes) {
+        for (node_name <- snapshot.node_files) {
+          val node = snapshot.get_node(node_name)
           val xml =
             snapshot.state.xml_markup(snapshot.version, node_name,
               elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -282,7 +282,7 @@
     pos match {
       case Position.Item_Id(id, range) if range.start > 0 =>
         snapshot.find_command(id) match {
-          case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
+          case Some((node, command)) if snapshot.get_node(command.node_name) eq node =>
             node.command_start(command) match {
               case Some(start) => text_offset == start + command.chunk.decode(range.start)
               case None => false
diff -r b09f358f3eb0 -r 18bc50e58e38 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Fri Dec 04 17:55:17 2020 +0000
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Sat Dec 05 19:30:37 2020 +0100
@@ -183,7 +183,7 @@
 
     val iterator =
       restriction match {
-        case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
+        case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name)))
         case None => snapshot.version.nodes.iterator
       }
     val nodes_timing1 =