clarified signature: prefer high-level Snapshot over low-level Command.State;

--- a/src/Pure/PIDE/document.scala	Thu Nov 26 15:18:09 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Nov 26 15:49:27 2020 +0100
@@ -569,7 +569,7 @@
           .define_version(version1, state0.the_assignment(version))
           .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
 
-      state1.snapshot()
+      state1.snapshot(name = node_name)
     }
 
     def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
@@ -814,10 +814,18 @@
         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 {
+    def end_theory(theory: String): (Snapshot, State) =
+      theories.collectFirst({ case (_, st) if st.command.node_name.theory == theory => st }) match {
         case None => fail
-        case Some((id, st)) => (st, copy(theories = theories - id))
+        case Some(st) =>
+          val command = st.command
+          val node_name = command.node_name
+          val command1 =
+            Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name,
+              results = st.results, markup = st.markup(Command.Markup_Index.markup))
+          val state1 = copy(theories = theories - command1.id)
+          val snapshot = state1.snapshot(name = node_name).command_snippet(command1)
+          (snapshot, state1)
       }
 
     def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)

--- a/src/Pure/PIDE/session.scala	Thu Nov 26 15:18:09 2020 +0100
+++ b/src/Pure/PIDE/session.scala	Thu Nov 26 15:49:27 2020 +0100
@@ -181,7 +181,7 @@
 
   /* outlets */
 
-  val finished_theories = new Session.Outlet[Command.State](dispatcher)
+  val finished_theories = new Session.Outlet[Document.Snapshot](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)
@@ -511,8 +511,8 @@
 
               case Markup.Finished_Theory(theory) =>
                 try {
-                  val st = global_state.change_result(_.end_theory(theory))
-                  finished_theories.post(st)
+                  val snapshot = global_state.change_result(_.end_theory(theory))
+                  finished_theories.post(snapshot)
                 }
                 catch { case _: Document.State.Fail => bad_output() }
 

--- a/src/Pure/Tools/build_job.scala	Thu Nov 26 15:18:09 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Nov 26 15:49:27 2020 +0100
@@ -157,21 +157,16 @@
           case Session.Runtime_Statistics(props) => runtime_statistics += props
         }
 
-      session.finished_theories += Session.Consumer[Command.State]("finished_theories")
+      session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories")
         {
-          case st =>
-            val command = st.command
-            val markup = st.markups(Command.Markup_Index.markup)
-
+          case snapshot =>
             def export(name: String, xml: XML.Body)
             {
-              val theory_name = command.node_name.theory
+              val theory_name = snapshot.node_name.theory
               val args = Protocol.Export.Args(theory_name = theory_name, name = name)
               export_consumer(session_name, args, Bytes(YXML.string_of_body(xml)))
             }
-
-            export(Export.MARKUP,
-              markup.to_XML(command.range, command.source, Markup.Elements.full))
+            export(Export.MARKUP, snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
         }
 
       session.all_messages += Session.Consumer[Any]("build_session_output")