src/Pure/PIDE/document.scala

               blobs_info = command.blobs_info, results = st.results, markups = st.markups)
           val state1 = copy(theories = theories - id)
           (state1.snippet(List(command1), doc_blobs), state1)
       }
 
+    def theory_snapshot(id: Document_ID.Exec, document_blobs: Node.Name => Blobs): Option[Snapshot] =
+      if (theories.isDefinedAt(id)) Some(end_theory(id, document_blobs)._1) else None
+
     def assign(
       id: Document_ID.Version,
       edited: List[String],
       update: Assign_Update
     ) : ((List[Node.Name], List[Command]), State) = {