--- a/src/Pure/PIDE/session.scala Thu Jan 05 12:43:05 2023 +0100
+++ b/src/Pure/PIDE/session.scala Thu Jan 05 16:44:15 2023 +0100
@@ -125,8 +125,8 @@
val cache: Term.Cache = Term.Cache.make()
- def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
- Command.Blobs_Info.none
+ def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none
+ def build_blobs(name: Document.Node.Name): Document.Blobs = Document.Blobs.empty
/* global flags */
@@ -560,7 +560,7 @@
case Markup.Process_Result(result) if output.is_exit =>
if (prover.defined) protocol_handlers.exit()
for (id <- global_state.value.theories.keys) {
- val snapshot = global_state.change_result(_.end_theory(id))
+ val snapshot = global_state.change_result(_.end_theory(id, build_blobs))
finished_theories.post(snapshot)
}
file_formats.stop_session()