# HG changeset patch
# User wenzelm
# Date 1606335225 -3600
# Node ID fabd29c73098bbd91870ca15883fcdf7c9f12858
# Parent  905abe2ed279971b33df840f4d83225ef12ec27b# Parent  d76b0f29c8fd4f08cb8b0170ad7bac39ef1fcf3e
merged

diff -r 905abe2ed279 -r fabd29c73098 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Admin/build_log.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -485,12 +485,10 @@
     val Session_Finished1 =
       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
     val Session_Finished2 =
-      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
+      new Regex("""^Finished ([^\s/]+) \((\d+):(\d+):(\d+) elapsed time.*$""")
     val Session_Timing =
       new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
-    val Session_Failed = new Regex("""^(\S+) FAILED""")
-    val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
     val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""")
     val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
 
@@ -514,8 +512,6 @@
     var timing = Map.empty[String, Timing]
     var ml_timing = Map.empty[String, Timing]
     var started = Set.empty[String]
-    var failed = Set.empty[String]
-    var cancelled = Set.empty[String]
     var sources = Map.empty[String, String]
     var heap_sizes = Map.empty[String, Long]
     var theory_timings = Map.empty[String, Map[String, Timing]]
@@ -524,7 +520,7 @@
 
     def all_sessions: Set[String] =
       chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
-      failed ++ cancelled ++ started ++ sources.keySet ++ heap_sizes.keySet ++
+      started ++ sources.keySet ++ heap_sizes.keySet ++
       theory_timings.keySet ++ ml_statistics.keySet
 
 
@@ -596,9 +592,7 @@
       Map(
         (for (name <- all_sessions.toList) yield {
           val status =
-            if (failed(name)) Session_Status.failed
-            else if (cancelled(name)) Session_Status.cancelled
-            else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
+            if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
               Session_Status.finished
             else if (started(name)) Session_Status.failed
             else Session_Status.existing
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/General/file.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -222,7 +222,7 @@
     val line =
       try { reader.readLine}
       catch { case _: IOException => null }
-    Option(line)
+    Option(line).map(Library.trim_line)
   }
 
   def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/General/position.ML	Wed Nov 25 21:13:45 2020 +0100
@@ -40,7 +40,6 @@
   val def_properties_of: T -> Properties.T
   val entity_markup: string -> string * T -> Markup.T
   val entity_properties_of: bool -> serial -> T -> Properties.T
-  val default_properties: T -> Properties.T -> Properties.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
   val is_reported_range: T -> bool
@@ -91,7 +90,7 @@
 
 fun norm_props (props: Properties.T) =
   maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
-    Markup.position_properties';
+    [Markup.fileN, Markup.idN];
 
 fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
@@ -211,10 +210,6 @@
   if def then (Markup.defN, Value.print_int serial) :: properties_of pos
   else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
 
-fun default_properties default props =
-  if exists (member (op =) Markup.position_properties o #1) props then props
-  else properties_of default @ props;
-
 val markup = Markup.properties o properties_of;
 
 
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/General/position.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -112,29 +112,12 @@
       }
   }
 
-  object Identified
-  {
-    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =
-      pos match {
-        case Id(id) =>
-          val chunk_name =
-            pos match {
-              case File(name) => Symbol.Text_Chunk.File(name)
-              case _ => Symbol.Text_Chunk.Default
-            }
-          Some((id, chunk_name))
-        case _ => None
-      }
-  }
-
-  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
-
 
   /* here: user output */
 
   def here(props: T, delimited: Boolean = true): String =
   {
-    val pos = props.filter(p => Markup.POSITION_PROPERTIES(p._1))
+    val pos = props.filter(Markup.position_property)
     if (pos.isEmpty) ""
     else {
       val s0 =
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -142,7 +142,7 @@
         Markup_Index(status, chunk_name)
       }
 
-      (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _)
+      (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML))(body))(_ + _)
     }
   }
 
@@ -331,55 +331,56 @@
         xml_cache: XML.Cache): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
-          (this /: msgs)((state, msg) =>
-            msg match {
-              case elem @ XML.Elem(markup, Nil) =>
-                state.
-                  add_status(markup).
-                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
-              case _ =>
-                Output.warning("Ignored status message: " + msg)
-                state
-            })
+          if (command.span.is_theory) this
+          else {
+            (this /: msgs)((state, msg) =>
+              msg match {
+                case elem @ XML.Elem(markup, Nil) =>
+                  state.
+                    add_status(markup).
+                    add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
+                case _ =>
+                  Output.warning("Ignored status message: " + msg)
+                  state
+              })
+          }
 
-        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
+        case XML.Elem(Markup(Markup.REPORT, atts0), msgs) =>
           (this /: msgs)((state, msg) =>
             {
               def bad(): Unit = Output.warning("Ignored report message: " + msg)
 
               msg match {
-                case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) =>
-
-                  val target =
-                    if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
-                      Some((chunk_name, command.chunks(chunk_name)))
-                    else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
-                    else None
+                case XML.Elem(Markup(name, atts1), args) =>
+                  val atts = atts1 ::: atts0
+                  command.reported_position(atts) match {
+                    case Some((id, chunk_name)) =>
+                      val target =
+                        if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
+                          Some((chunk_name, command.chunks(chunk_name)))
+                        else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
+                        else None
 
-                  (target, atts) match {
-                    case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
-                      target_chunk.incorporate(symbol_range) match {
-                        case Some(range) =>
-                          val props = Position.purge(atts)
-                          val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
-                          state.add_markup(false, target_name, Text.Info(range, elem))
-                        case None => bad(); state
+                      (target, atts) match {
+                        case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
+                          target_chunk.incorporate(symbol_range) match {
+                            case Some(range) =>
+                              val props = atts.filterNot(Markup.position_property)
+                              val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
+                              state.add_markup(false, target_name, Text.Info(range, elem))
+                            case None => bad(); state
+                          }
+                        case _ =>
+                          // silently ignore excessive reports
+                          state
                       }
-                    case _ =>
-                      // silently ignore excessive reports
-                      state
+
+                    case _ => bad(); state
                   }
-
-                case XML.Elem(Markup(name, atts), args)
-                if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
-                  val range = command.core_range
-                  val props = Position.purge(atts)
-                  val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
-                  state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem))
-
                 case _ => bad(); state
               }
             })
+
         case XML.Elem(Markup(name, props), body) =>
           props match {
             case Markup.Serial(i) =>
@@ -392,8 +393,7 @@
               if (Protocol.is_inlined(message)) {
                 for {
                   (chunk_name, chunk) <- command.chunks.iterator
-                  range <- Protocol_Message.positions(
-                    self_id, command.span.position, chunk_name, chunk, message)
+                  range <- command.message_positions(self_id, chunk_name, chunk, message)
                 } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup))
               }
               st
@@ -425,24 +425,21 @@
     Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty)
 
   def unparsed(
-    id: Document_ID.Command,
     source: String,
-    results: Results,
-    markup: Markup_Tree): Command =
+    theory: Boolean = false,
+    id: Document_ID.Command = Document_ID.none,
+    node_name: Document.Node.Name = Document.Node.Name.empty,
+    results: Results = Results.empty,
+    markup: Markup_Tree = Markup_Tree.empty): Command =
   {
-    val (source1, span1) = Command_Span.unparsed(source).compact_source
-    new Command(id, Document.Node.Name.empty, no_blobs, span1, source1, results, markup)
+    val (source1, span1) = Command_Span.unparsed(source, theory).compact_source
+    new Command(id, node_name, no_blobs, span1, source1, results, markup)
   }
 
-  def text(source: String): Command =
-    unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
+  def text(source: String): Command = unparsed(source)
 
   def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
-  {
-    val text = XML.content(body)
-    val markup = Markup_Tree.from_XML(body)
-    unparsed(id, text, results, markup)
-  }
+    unparsed(XML.content(body), id = id, results = results, markup = Markup_Tree.from_XML(body))
 
 
   /* perspective */
@@ -614,6 +611,61 @@
   def source(range: Text.Range): String = range.substring(source)
 
 
+  /* reported positions */
+
+  def reported_position(pos: Position.T): Option[(Document_ID.Generic, Symbol.Text_Chunk.Name)] =
+    pos match {
+      case Position.Id(id) =>
+        val chunk_name =
+          pos match {
+            case Position.File(name) if name != node_name.node =>
+              Symbol.Text_Chunk.File(name)
+            case _ => Symbol.Text_Chunk.Default
+          }
+        Some((id, chunk_name))
+      case _ => None
+    }
+
+  def message_positions(
+    self_id: Document_ID.Generic => Boolean,
+    chunk_name: Symbol.Text_Chunk.Name,
+    chunk: Symbol.Text_Chunk,
+    message: XML.Elem): Set[Text.Range] =
+  {
+    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 =>
+          val opt_range =
+            Position.Range.unapply(props) orElse {
+              if (name == Symbol.Text_Chunk.Default)
+                Position.Range.unapply(span.position)
+              else None
+            }
+          opt_range match {
+            case Some(symbol_range) =>
+              chunk.incorporate(symbol_range) match {
+                case Some(range) => set + range
+                case _ => set
+              }
+            case None => set
+          }
+        case _ => set
+      }
+    def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
+      t match {
+        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
+          body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree)
+        case XML.Elem(Markup(name, props), body) =>
+          body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree)
+        case XML.Text(_) => set
+      }
+
+    val set = tree(Set.empty, message)
+    if (set.isEmpty) elem(message.markup.properties, set)
+    else set
+  }
+
+
   /* accumulated results */
 
   val init_state: Command.State =
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -18,14 +18,18 @@
         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 object Ignored_Span extends Kind
   case object Malformed_Span extends Kind
+  case object Theory_Span extends Kind
 
   sealed case class Span(kind: Kind, content: List[Token])
   {
+    def is_theory: Boolean = kind == Theory_Span
+
     def name: String =
       kind match { case Command_Span(name, _) => name case _ => "" }
 
@@ -67,8 +71,11 @@
 
   val empty: Span = Span(Ignored_Span, Nil)
 
-  def unparsed(source: String): Span =
-    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
+  def unparsed(source: String, theory: Boolean): Span =
+  {
+    val kind = if (theory) Theory_Span else Malformed_Span
+    Span(kind, List(Token(Token.Kind.UNPARSED, source)))
+  }
 
 
   /* XML data representation */
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -672,6 +672,8 @@
     versions: Map[Document_ID.Version, Version] = Map.empty,
     /*inlined auxiliary files*/
     blobs: Set[SHA1.Digest] = Set.empty,
+    /*loaded theories in batch builds*/
+    theories: Map[Document_ID.Exec, Command.State] = Map.empty,
     /*static markup from define_command*/
     commands: Map[Document_ID.Command, Command.State] = Map.empty,
     /*dynamic markup from execution*/
@@ -721,7 +723,7 @@
     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
 
     def lookup_id(id: Document_ID.Generic): Option[Command.State] =
-      commands.get(id) orElse execs.get(id)
+      theories.get(id) orElse commands.get(id) orElse execs.get(id)
 
     private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
       id == st.command.id ||
@@ -738,18 +740,21 @@
     def accumulate(id: Document_ID.Generic, message: XML.Elem, xml_cache: XML.Cache)
       : (Command.State, State) =
     {
-      execs.get(id) match {
-        case Some(st) =>
-          val new_st = st.accumulate(self_id(st), other_id, message, xml_cache)
-          val execs1 = execs + (id -> new_st)
-          (new_st, copy(execs = execs1, commands_redirection = redirection(new_st)))
+      def update(st: Command.State): (Command.State, State) =
+      {
+        val st1 = st.accumulate(self_id(st), other_id, message, xml_cache)
+        (st1, copy(commands_redirection = redirection(st1)))
+      }
+      execs.get(id).map(update) match {
+        case Some((st1, state1)) => (st1, state1.copy(execs = execs + (id -> st1)))
         case None =>
-          commands.get(id) match {
-            case Some(st) =>
-              val new_st = st.accumulate(self_id(st), other_id, message, xml_cache)
-              val commands1 = commands + (id -> new_st)
-              (new_st, copy(commands = commands1, commands_redirection = redirection(new_st)))
-            case None => fail
+          commands.get(id).map(update) match {
+            case Some((st1, state1)) => (st1, state1.copy(commands = commands + (id -> st1)))
+            case None =>
+              theories.get(id).map(update) match {
+                case Some((st1, state1)) => (st1, state1.copy(theories = theories + (id -> st1)))
+                case None => fail
+              }
           }
       }
     }
@@ -781,6 +786,19 @@
           st <- command_states(version, command).iterator
         } yield st.exports)
 
+    def begin_theory(node_name: Node.Name, id: Document_ID.Exec, source: String): State =
+      if (theories.isDefinedAt(id)) fail
+      else {
+        val command = Command.unparsed(source, theory = true, id = id, node_name = node_name)
+        copy(theories = theories + (id -> command.empty_state))
+      }
+
+    def end_theory(theory: String): (Command.State, State) =
+      theories.find({ case (_, st) => st.command.node_name.theory == theory }) match {
+        case None => fail
+        case Some((id, st)) => (st, copy(theories = theories - id))
+      }
+
     def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
       : ((List[Node.Name], List[Command]), State) =
     {
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Nov 25 21:13:45 2020 +0100
@@ -59,8 +59,8 @@
   val end_offsetN: string
   val fileN: string
   val idN: string
-  val position_properties': string list
   val position_properties: string list
+  val position_property: Properties.entry -> bool
   val positionN: string val position: T
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
@@ -220,6 +220,7 @@
   val theory_timing: Properties.entry
   val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
+  val finished_theory: string -> Properties.T
   val build_session_finished: Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
@@ -379,8 +380,8 @@
 val fileN = "file";
 val idN = "id";
 
-val position_properties' = [fileN, idN];
-val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
+val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
+fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
 
 val (positionN, position) = markup_elem "position";
 
@@ -692,7 +693,8 @@
 
 val session_timing = (functionN, "session_timing");
 
-fun loading_theory name = [("function", "loading_theory"), ("name", name)];
+fun loading_theory name = [("function", "loading_theory"), (nameN, name)];
+fun finished_theory name = [("function", "finished_theory"), (nameN, name)];
 
 val build_session_finished = [("function", "build_session_finished")];
 
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -144,6 +144,8 @@
   val DEF_ID = "def_id"
 
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
+  def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
+
   val POSITION = "position"
 
 
@@ -587,6 +589,7 @@
   }
 
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
+  def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
@@ -596,7 +599,8 @@
   }
   object Task_Statistics extends Properties_Function("task_statistics")
 
-  object Loading_Theory extends Name_Function("loading_theory")
+  object Loading_Theory extends Properties_Function("loading_theory")
+  object Finished_Theory extends Name_Function("finished_theory")
   object Build_Session_Finished extends Function("build_session_finished")
 
   object Commands_Accepted extends Function("commands_accepted")
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -21,6 +21,21 @@
   val Error_Message_Marker = Protocol_Message.Marker("error_message")
 
 
+  /* batch build */
+
+  object Loading_Theory
+  {
+    def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] =
+      (props, props, props) match {
+        case (Markup.Name(name), Position.File(file), Position.Id(id))
+        if Path.is_wellformed(file) =>
+          val master_dir = Path.explode(file).dir.implode
+          Some((Document.Node.Name(file, master_dir, name), id))
+        case _ => None
+      }
+  }
+
+
   /* document editing */
 
   object Commands_Accepted
@@ -188,13 +203,13 @@
   object Export
   {
     sealed case class Args(
-      id: Option[String],
-      serial: Long,
+      id: Option[String] = None,
+      serial: Long = 0L,
       theory_name: String,
       name: String,
-      executable: Boolean,
-      compress: Boolean,
-      strict: Boolean)
+      executable: Boolean = false,
+      compress: Boolean = true,
+      strict: Boolean = true)
     {
       def compound_name: String = isabelle.Export.compound_name(theory_name, name)
     }
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/PIDE/protocol_message.scala
--- a/src/Pure/PIDE/protocol_message.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/protocol_message.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -71,50 +71,4 @@
       case XML.Elem(_, ts) => reports(props, ts)
       case XML.Text(_) => Nil
     }
-
-
-  /* reported positions */
-
-  private val position_elements =
-    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
-
-  def positions(
-    self_id: Document_ID.Generic => Boolean,
-    command_position: Position.T,
-    chunk_name: Symbol.Text_Chunk.Name,
-    chunk: Symbol.Text_Chunk,
-    message: XML.Elem): Set[Text.Range] =
-  {
-    def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
-      props match {
-        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
-          val opt_range =
-            Position.Range.unapply(props) orElse {
-              if (name == Symbol.Text_Chunk.Default)
-                Position.Range.unapply(command_position)
-              else None
-            }
-          opt_range match {
-            case Some(symbol_range) =>
-              chunk.incorporate(symbol_range) match {
-                case Some(range) => set + range
-                case _ => set
-              }
-            case None => set
-          }
-        case _ => set
-      }
-    def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
-      t match {
-        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
-          body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
-        case XML.Elem(Markup(name, props), body) =>
-          body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
-        case XML.Text(_) => set
-      }
-
-    val set = tree(Set.empty, message)
-    if (set.isEmpty) elem(message.markup.properties, set)
-    else set
-  }
 }
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -169,6 +169,9 @@
 
   /* markup elements */
 
+  val position_elements =
+    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+
   val semantic_completion_elements =
     Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
 
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/session.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -181,6 +181,7 @@
 
   /* outlets */
 
+  val finished_theories = new Session.Outlet[Command.State](dispatcher)
   val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher)
   val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher)
   val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher)
@@ -475,7 +476,9 @@
       {
         try {
           val st = global_state.change_result(f)
-          change_buffer.invoke(false, Nil, List(st.command))
+          if (!st.command.span.is_theory) {
+            change_buffer.invoke(false, Nil, List(st.command))
+          }
         }
         catch { case _: Document.State.Fail => bad_output() }
       }
@@ -502,6 +505,17 @@
                 val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
                 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)) }
+                catch { case _: Document.State.Fail => bad_output() }
+
+              case Markup.Finished_Theory(theory) =>
+                try {
+                  val st = global_state.change_result(_.end_theory(theory))
+                  finished_theories.post(st)
+                }
+                catch { case _: Document.State.Fail => bad_output() }
+
               case List(Markup.Commands_Accepted.PROPERTY) =>
                 msg.text match {
                   case Protocol.Commands_Accepted(ids) =>
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/ROOT.ML	Wed Nov 25 21:13:45 2020 +0100
@@ -352,3 +352,4 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML"
+
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Nov 25 21:13:45 2020 +0100
@@ -148,11 +148,10 @@
       if forall (fn s => s = "") ss then ()
       else
         let
-          val props' =
-            (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
-              (false, SOME id') => props @ [(Markup.idN, id')]
-            | _ => props);
-        in message name props' (XML.blob ss) end;
+          val pos_props =
+            if exists Markup.position_property props then props
+            else props @ Position.properties_of (Position.thread_data ());
+        in message name pos_props (XML.blob ss) end;
 
     fun report_message ss =
       if Context_Position.pide_reports ()
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/System/progress.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -32,7 +32,6 @@
 
   def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
   def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
-  def echo_document(msg: String) { echo(msg) }
 
   def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
     Timing.timeit(message, enabled, echo)(e)
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Thy/export.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -13,7 +13,13 @@
 
 object Export
 {
-  /* name structure */
+  /* artefact names */
+
+  val MARKUP = "PIDE/markup"
+  val MESSAGES = "PIDE/messages"
+  val DOCUMENT_PREFIX = "document/"
+  val THEORY_PREFIX: String = "theory/"
+  val PROOFS_PREFIX: String = "proofs/"
 
   def explode_name(s: String): List[String] = space_explode('/', s)
   def implode_name(elems: Iterable[String]): String = elems.mkString("/")
@@ -89,6 +95,7 @@
 
     def compound_name: String = Export.compound_name(theory_name, name)
 
+    def name_has_prefix(s: String): Boolean = name.startsWith(s)
     val name_elems: List[String] = explode_name(name)
 
     def name_extends(elems: List[String]): Boolean =
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Thy/export_theory.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -62,9 +62,6 @@
 
   /** theory content **/
 
-  val export_prefix: String = "theory/"
-  val export_prefix_proofs: String = "proofs/"
-
   sealed case class Theory(name: String, parents: List[String],
     types: List[Type],
     consts: List[Const],
@@ -115,7 +112,7 @@
     val parents =
       if (theory_name == Thy_Header.PURE) Nil
       else {
-        provider(export_prefix + "parents") match {
+        provider(Export.THEORY_PREFIX + "parents") match {
           case Some(entry) => split_lines(entry.uncompressed().text)
           case None =>
             error("Missing theory export in session " + quote(session_name) + ": " +
@@ -195,7 +192,7 @@
       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
         val name = Markup.Name.unapply(props) getOrElse err()
         val xname = Markup.XName.unapply(props) getOrElse err()
-        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
+        val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID)
         val id = Position.Id.unapply(props)
         val serial = Markup.Serial.unapply(props) getOrElse err()
         (Entity(kind, name, xname, pos, id, serial), body)
@@ -239,7 +236,7 @@
   }
 
   def read_types(provider: Export.Provider): List[Type] =
-    provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "types").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.TYPE, tree)
         val (syntax, args, abbrev) =
@@ -271,7 +268,7 @@
   }
 
   def read_consts(provider: Export.Provider): List[Const] =
-    provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "consts").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.CONST, tree)
         val (syntax, (typargs, (typ, (abbrev, propositional)))) =
@@ -318,7 +315,7 @@
   }
 
   def read_axioms(provider: Export.Provider): List[Axiom] =
-    provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "axioms").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.AXIOM, tree)
         val prop = decode_prop(body)
@@ -348,7 +345,7 @@
   }
 
   def read_thms(provider: Export.Provider): List[Thm] =
-    provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "thms").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.THM, tree)
         val (prop, deps, prf) =
@@ -379,7 +376,7 @@
   def read_proof(
     provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
   {
-    for { entry <- provider.focus(id.theory_name)(export_prefix_proofs + id.serial) }
+    for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) }
     yield {
       val body = entry.uncompressed_yxml()
       val (typargs, (args, (prop_body, proof_body))) =
@@ -454,7 +451,7 @@
   }
 
   def read_classes(provider: Export.Provider): List[Class] =
-    provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "classes").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.CLASS, tree)
         val (params, axioms) =
@@ -483,7 +480,7 @@
   }
 
   def read_locales(provider: Export.Provider): List[Locale] =
-    provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "locales").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.LOCALE, tree)
         val (typargs, args, axioms) =
@@ -520,7 +517,7 @@
   }
 
   def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] =
-    provider.uncompressed_yxml(export_prefix + "locale_dependencies").map((tree: XML.Tree) =>
+    provider.uncompressed_yxml(Export.THEORY_PREFIX + "locale_dependencies").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.LOCALE_DEPENDENCY, tree)
         val (source, (target, (prefix, (subst_types, subst_terms)))) =
@@ -544,7 +541,7 @@
 
   def read_classrel(provider: Export.Provider): List[Classrel] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "classrel")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "classrel")
     val classrel =
     {
       import XML.Decode._
@@ -562,7 +559,7 @@
 
   def read_arities(provider: Export.Provider): List[Arity] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "arities")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "arities")
     val arities =
     {
       import XML.Decode._
@@ -583,7 +580,7 @@
 
   def read_constdefs(provider: Export.Provider): List[Constdef] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "constdefs")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs")
     val constdefs =
     {
       import XML.Decode._
@@ -609,7 +606,7 @@
 
   def read_typedefs(provider: Export.Provider): List[Typedef] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "typedefs")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs")
     val typedefs =
     {
       import XML.Decode._
@@ -645,7 +642,7 @@
 
   def read_datatypes(provider: Export.Provider): List[Datatype] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "datatypes")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes")
     val datatypes =
     {
       import XML.Decode._
@@ -741,7 +738,7 @@
 
   def read_spec_rules(provider: Export.Provider): List[Spec_Rule] =
   {
-    val body = provider.uncompressed_yxml(export_prefix + "spec_rules")
+    val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules")
     val spec_rules =
     {
       import XML.Decode._
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -12,9 +12,15 @@
 
 object Presentation
 {
-  /* document variants */
+  /* document info */
 
-  type Document_PDF = (Document_Variant, Bytes)
+  abstract class Document_Name
+  {
+    def name: String
+    def path: Path = Path.basic(name)
+
+    override def toString: String = name
+  }
 
   object Document_Variant
   {
@@ -29,13 +35,11 @@
       }
   }
 
-  sealed case class Document_Variant(name: String, tags: List[String], sources: String = "")
+  sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name
   {
     def print_tags: String = tags.mkString(",")
     def print: String = if (tags.isEmpty) name else name + "=" + print_tags
 
-    def path: Path = Path.basic(name)
-
     def latex_sty: String =
       Library.terminate_lines(
         tags.map(tag =>
@@ -45,8 +49,19 @@
             case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
             case cs => "\\isakeeptag{" + cs.mkString + "}"
           }))
+  }
 
-    def set_sources(s: String): Document_Variant = copy(sources = s)
+  sealed case class Document_Input(name: String, sources: SHA1.Digest)
+    extends Document_Name
+
+  sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes)
+    extends Document_Name
+  {
+    def log: String = log_xz.uncompress().text
+    def log_lines: List[String] = split_lines(log)
+
+    def write(db: SQL.Database, session_name: String) =
+      write_document(db, session_name, this)
   }
 
 
@@ -56,32 +71,30 @@
   {
     val session_name = SQL.Column.string("session_name").make_primary_key
     val name = SQL.Column.string("name").make_primary_key
-    val tags = SQL.Column.string("tags")
     val sources = SQL.Column.string("sources")
+    val log_xz = SQL.Column.bytes("log_xz")
     val pdf = SQL.Column.bytes("pdf")
 
-    val table = SQL.Table("isabelle_documents", List(session_name, name, tags, sources, pdf))
+    val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
       "WHERE " + Data.session_name.equal(session_name) +
         (if (name == "") "" else " AND " + Data.name.equal(name))
   }
 
-  def read_document_variants(db: SQL.Database, session_name: String): List[Document_Variant] =
+  def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
   {
-    val select =
-      Data.table.select(List(Data.name, Data.tags, Data.sources), Data.where_equal(session_name))
+    val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name))
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(res =>
       {
         val name = res.string(Data.name)
-        val tags = res.string(Data.tags)
         val sources = res.string(Data.sources)
-        Document_Variant.parse(name, tags).set_sources(sources)
+        Document_Input(name, SHA1.fake(sources))
       }).toList)
   }
 
-  def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_PDF] =
+  def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] =
   {
     val select = Data.table.select(sql = Data.where_equal(session_name, name))
     db.using_statement(select)(stmt =>
@@ -89,24 +102,24 @@
       val res = stmt.execute_query()
       if (res.next()) {
         val name = res.string(Data.name)
-        val tags = res.string(Data.tags)
         val sources = res.string(Data.sources)
+        val log_xz = res.bytes(Data.log_xz)
         val pdf = res.bytes(Data.pdf)
-        Some(Document_Variant.parse(name, tags).set_sources(sources) -> pdf)
+        Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf))
       }
       else None
     })
   }
 
-  def write_document(db: SQL.Database, session_name: String, doc: Document_Variant, pdf: Bytes)
+  def write_document(db: SQL.Database, session_name: String, doc: Document_Output)
   {
     db.using_statement(Data.table.insert())(stmt =>
     {
       stmt.string(1) = session_name
       stmt.string(2) = doc.name
-      stmt.string(3) = doc.print_tags
-      stmt.string(4) = doc.sources
-      stmt.bytes(5) = pdf
+      stmt.string(3) = doc.sources.toString
+      stmt.bytes(4) = doc.log_xz
+      stmt.bytes(5) = doc.pdf
       stmt.execute()
     })
   }
@@ -253,8 +266,8 @@
     val documents =
       for {
         doc <- info.document_variants
-        (_, pdf) <- db_context.read_document(session, doc.name)
-      } yield { Bytes.write(session_dir + doc.path.pdf, pdf); doc }
+        document <- db_context.read_document(session, doc.name)
+      } yield { Bytes.write(session_dir + doc.path.pdf, document.pdf); doc }
 
     val links =
     {
@@ -443,7 +456,7 @@
     output_sources: Option[Path] = None,
     output_pdf: Option[Path] = None,
     verbose: Boolean = false,
-    verbose_latex: Boolean = false): List[Document_PDF] =
+    verbose_latex: Boolean = false): List[Document_Output] =
   {
     /* session info */
 
@@ -499,7 +512,7 @@
       yield {
         Isabelle_System.with_tmp_dir("document")(tmp_dir =>
         {
-          progress.echo_document("Building document " + session + "/" + doc.name + " ...")
+          progress.echo("Preparing " + session + "/" + doc.name + " ...")
           val start = Time.now()
 
 
@@ -507,7 +520,7 @@
 
           val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
           val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
-          val sources = SHA1.digest_set(digests).toString
+          val sources = SHA1.digest_set(digests)
           prepare_dir2(tmp_dir, doc)
 
           for (dir <- output_sources) {
@@ -520,12 +533,12 @@
 
           val old_document =
             for {
-              document@(doc, pdf) <- db_context.read_document(session, doc.name)
-              if doc.sources == sources
+              old_doc <- db_context.read_document(session, doc.name)
+              if old_doc.sources == sources
             }
             yield {
-              Bytes.write(doc_dir + doc.path.pdf, pdf)
-              document
+              Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf)
+              old_doc
             }
 
           old_document getOrElse {
@@ -574,20 +587,22 @@
             else {
               val stop = Time.now()
               val timing = stop - start
-              progress.echo_document("Finished document " + session + "/" + doc.name +
+              progress.echo("Finished " + session + "/" + doc.name +
                 " (" + timing.message_hms + " elapsed time)")
 
-              doc.set_sources(sources) -> Bytes.read(result_path)
+              val log_xz = Bytes(cat_lines(result.out_lines ::: result.err_lines)).compress()
+              val pdf = Bytes.read(result_path)
+              Document_Output(doc.name, sources, log_xz, pdf)
             }
           }
         })
       }
 
-    for (dir <- output_pdf; (doc, pdf) <- documents) {
+    for (dir <- output_pdf; doc <- documents) {
       Isabelle_System.make_directory(dir)
       val path = dir + doc.path.pdf
-      Bytes.write(path, pdf)
-      progress.echo_document("Document at " + path.absolute)
+      Bytes.write(path, doc.pdf)
+      progress.echo("Document at " + path.absolute)
     }
 
     documents
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -1211,7 +1211,7 @@
       read_export(session, theory_name, name) getOrElse
         Export.empty_entry(session, theory_name, name)
 
-    def read_document(session_name: String, name: String): Option[Presentation.Document_PDF] =
+    def read_document(session_name: String, name: String): Option[Presentation.Document_Output] =
       database_server match {
         case Some(db) => Presentation.read_document(db, session_name, name)
         case None =>
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Nov 25 21:13:45 2020 +0100
@@ -56,7 +56,8 @@
 );
 
 fun apply_presentation (context: presentation_context) thy =
-  ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
+ (ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
+  Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) []);
 
 fun add_presentation f = Presentation.map (cons (f, stamp ()));
 
@@ -292,7 +293,7 @@
     val thy = Toplevel.end_theory end_pos end_state;
   in (results, thy) end;
 
-fun eval_thy options update_time master_dir header text_pos text parents =
+fun eval_thy options master_dir header text_pos text parents =
   let
     val (name, _) = #name header;
     val keywords =
@@ -324,30 +325,32 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy options initiators update_time deps text (name, pos) keywords parents =
+fun load_thy options initiators deps text (name, pos) keywords parents =
   let
-    val _ = remove_thy name;
-    val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
-    val _ = Output.try_protocol_message (Markup.loading_theory name) [];
+    val exec_id = Document_ID.make ();
+    val id = Document_ID.print exec_id;
+    val _ =
+      Execution.running Document_ID.none exec_id [] orelse
+        raise Fail ("Failed to register execution: " ^ id);
 
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
     val header = Thy_Header.make (name, pos) imports keywords;
-
     val _ =
       (imports ~~ parents) |> List.app (fn ((_, pos), thy) =>
         Context_Position.reports_global thy [(pos, Theory.get_markup thy)]);
 
-    val exec_id = Document_ID.make ();
-    val _ =
-      Execution.running Document_ID.none exec_id [] orelse
-        raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
+    val text_pos = Position.put_id id (Path.position thy_path);
+    val text_props = Position.properties_of text_pos;
+
+    val _ = remove_thy name;
+    val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
+    val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) (XML.blob [text]);
 
     val timing_start = Timing.start ();
 
-    val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
-      eval_thy options update_time dir header text_pos text
+      eval_thy options dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
 
     val timing_result = Timing.result timing_start;
@@ -411,12 +414,8 @@
               (case deps of
                 NONE => raise Fail "Malformed deps"
               | SOME (dep, text) =>
-                  let
-                    val update_time = serial ();
-                    val load =
-                      load_thy options initiators update_time
-                        dep text (theory_name, theory_pos) keywords;
-                  in Task (parents, load) end);
+                  Task (parents,
+                    load_thy options initiators dep text (theory_name, theory_pos) keywords));
 
           val tasks'' = new_entry theory_name parents task tasks';
         in (all_current, tasks'') end)
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Tools/build.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -202,7 +202,7 @@
       options +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
-        "pide_reports=false"
+        "pide_reports=false"  // FIXME
 
     val store = Sessions.store(build_options)
 
@@ -429,7 +429,7 @@
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
-                    new Build_Job(progress, session_name, info, deps, store, do_store, presentation,
+                    new Build_Job(progress, session_name, info, deps, store, do_store,
                       verbose, numa_node, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -16,7 +16,6 @@
   deps: Sessions.Deps,
   store: Sessions.Store,
   do_store: Boolean,
-  presentation: Presentation.Context,
   verbose: Boolean,
   val numa_node: Option[Int],
   command_timings0: List[Properties.T])
@@ -77,7 +76,6 @@
       val session_timings = new mutable.ListBuffer[Properties.T]
       val runtime_statistics = new mutable.ListBuffer[Properties.T]
       val task_statistics = new mutable.ListBuffer[Properties.T]
-      val document_output = new mutable.ListBuffer[String]
 
       def fun(
         name: String,
@@ -120,9 +118,9 @@
 
           private def loading_theory(msg: Prover.Protocol_Output): Boolean =
             msg.properties match {
-              case Markup.Loading_Theory(name) =>
+              case Markup.Loading_Theory(Markup.Name(name)) =>
                 progress.theory(Progress.Theory(name, session = session_name))
-                true
+                false
               case _ => false
             }
 
@@ -134,30 +132,43 @@
               case _ => false
             }
 
-          private def command_timing(props: Properties.T): Option[Properties.T] =
-            for {
-              props1 <- Markup.Command_Timing.unapply(props)
-              elapsed <- Markup.Elapsed.unapply(props1)
-              elapsed_time = Time.seconds(elapsed)
-              if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
-            } yield props1.filter(p => Markup.command_timing_properties(p._1))
-
           override val functions =
             List(
               Markup.Build_Session_Finished.name -> build_session_finished,
               Markup.Loading_Theory.name -> loading_theory,
               Markup.EXPORT -> export,
-              fun(Markup.Command_Timing.name, command_timings, command_timing),
               fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
               fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
               fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
         })
 
+      session.command_timings += Session.Consumer("command_timings")
+        {
+          case Session.Command_Timing(props) =>
+            for {
+              elapsed <- Markup.Elapsed.unapply(props)
+              elapsed_time = Time.seconds(elapsed)
+              if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
+            } command_timings += props.filter(Markup.command_timing_property)
+        }
+
       session.runtime_statistics += Session.Consumer("ML_statistics")
         {
           case Session.Runtime_Statistics(props) => runtime_statistics += props
         }
 
+      session.finished_theories += Session.Consumer[Command.State]("finished_theories")
+        {
+          case st =>
+            val command = st.command
+            val theory_name = command.node_name.theory
+            val args = Protocol.Export.Args(theory_name = theory_name, name = Export.MARKUP)
+            val xml =
+              st.markups(Command.Markup_Index.markup)
+                .to_XML(command.range, command.source, Markup.Elements.full)
+            export_consumer(session_name, args, Bytes(YXML.string_of_body(xml)))
+        }
+
       session.all_messages += Session.Consumer[Any]("build_session_output")
         {
           case msg: Prover.Output =>
@@ -212,38 +223,29 @@
       val process_result =
         Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
 
+      session.stop()
+
       val export_errors =
         export_consumer.shutdown(close = true).map(Output.error_message_text)
 
-      val document_errors =
+      val (document_output, document_errors) =
         try {
           if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
           {
-            val document_progress =
-              new Progress {
-                override def echo(msg: String): Unit =
-                  document_output.synchronized { document_output += msg }
-                override def echo_document(msg: String): Unit =
-                  progress.echo_document(msg)
-              }
             val documents =
               using(store.open_database_context(deps.sessions_structure))(db_context =>
                 Presentation.build_documents(session_name, deps, db_context,
                   output_sources = info.document_output,
                   output_pdf = info.document_output,
-                  progress = document_progress,
-                  verbose = verbose,
-                  verbose_latex = true))
+                  progress = progress,
+                  verbose = verbose))
             using(store.open_database(session_name, output = true))(db =>
-              for ((doc, pdf) <- documents) {
-                db.transaction {
-                  Presentation.write_document(db, session_name, doc, pdf)
-                }
-              })
+              documents.foreach(_.write(db, session_name)))
+            (documents.flatMap(_.log_lines), Nil)
           }
-          Nil
+          (Nil, Nil)
         }
-        catch { case Exn.Interrupt.ERROR(msg) => List(msg) }
+        catch { case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) }
 
       val result =
       {
@@ -256,7 +258,7 @@
             session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
-            document_output.toList
+            document_output
 
         val more_errors =
           Library.trim_line(stderr.toString) :: export_errors ::: document_errors
diff -r 905abe2ed279 -r fabd29c73098 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Tools/dump.scala	Wed Nov 25 21:13:45 2020 +0100
@@ -49,24 +49,26 @@
     List(
       Aspect("markup", "PIDE markup (YXML format)",
         { case args =>
-            args.write(Path.explode("markup.yxml"),
+            args.write(Path.explode(Export.MARKUP),
               args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
         }),
       Aspect("messages", "output messages (YXML format)",
         { case args =>
-            args.write(Path.explode("messages.yxml"),
+            args.write(Path.explode(Export.MESSAGES),
               args.snapshot.messages.iterator.map(_._1).toList)
         }),
       Aspect("latex", "generated LaTeX source",
         { case args =>
-            for (entry <- args.snapshot.exports if entry.name == "document.tex")
-              args.write(Path.explode(entry.name), entry.uncompressed())
+            for {
+              entry <- args.snapshot.exports
+              if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
+            } args.write(Path.explode(entry.name), entry.uncompressed())
         }),
       Aspect("theory", "foundational theory content",
         { case args =>
             for {
               entry <- args.snapshot.exports
-              if entry.name.startsWith(Export_Theory.export_prefix)
+              if entry.name_has_prefix(Export.THEORY_PREFIX)
             } args.write(Path.explode(entry.name), entry.uncompressed())
         }, options = List("export_theory"))
     ).sortBy(_.name)