support for PIDE markup in batch build (inactive due to pide_reports=false);
authorwenzelm
Mon, 23 Nov 2020 15:14:58 +0100
changeset 72928 22aeec526ffd
parent 72927 2126cf946086
child 72929 0201ae367518
support for PIDE markup in batch build (inactive due to pide_reports=false);
src/Pure/General/position.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/command_span.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/protocol_message.scala
src/Pure/PIDE/rendering.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.scala
src/Pure/Tools/build_job.scala
--- a/src/Pure/General/position.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/General/position.scala	Mon Nov 23 15:14:58 2020 +0100
@@ -112,21 +112,6 @@
       }
   }
 
-  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))
 
 
--- a/src/Pure/PIDE/command.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Nov 23 15:14:58 2020 +0100
@@ -331,16 +331,19 @@
         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) =>
           (this /: msgs)((state, msg) =>
@@ -348,38 +351,42 @@
               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, atts), args) =>
+                  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 = 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
+                          }
+                        case _ =>
+                          // silently ignore excessive reports
+                          state
                       }
-                    case _ =>
-                      // silently ignore excessive reports
-                      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 None
+                    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 _ => bad(); state
               }
             })
+
         case XML.Elem(Markup(name, props), body) =>
           props match {
             case Markup.Serial(i) =>
@@ -392,8 +399,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 +431,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 +617,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 =
--- a/src/Pure/PIDE/command_span.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala	Mon Nov 23 15:14:58 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 */
--- a/src/Pure/PIDE/document.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Nov 23 15:14:58 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) =
     {
--- a/src/Pure/PIDE/markup.ML	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Nov 23 15:14:58 2020 +0100
@@ -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
@@ -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")];
 
--- a/src/Pure/PIDE/markup.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Nov 23 15:14:58 2020 +0100
@@ -596,7 +596,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")
--- a/src/Pure/PIDE/protocol.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Nov 23 15:14:58 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)
     }
--- a/src/Pure/PIDE/protocol_message.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/protocol_message.scala	Mon Nov 23 15:14:58 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
-  }
 }
--- a/src/Pure/PIDE/rendering.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Nov 23 15:14:58 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)
 
--- a/src/Pure/PIDE/session.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/session.scala	Mon Nov 23 15:14:58 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) =>
--- a/src/Pure/Thy/thy_info.ML	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Nov 23 15:14:58 2020 +0100
@@ -62,6 +62,7 @@
 
 val _ =
   Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
+   (Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) [];
     if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
@@ -76,7 +77,7 @@
             val latex = Latex.isabelle_body thy_name body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
           in Export.export thy document_tex_name (XML.blob output) end
-      end));
+      end)));
 
 
 
@@ -326,26 +327,28 @@
 
 fun load_thy options initiators update_time 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
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
--- a/src/Pure/Tools/build.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/Tools/build.scala	Mon Nov 23 15:14:58 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)
 
--- a/src/Pure/Tools/build_job.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Nov 23 15:14:58 2020 +0100
@@ -120,9 +120,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
             }
 
@@ -158,6 +158,18 @@
           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 =>