--- a/src/Pure/Tools/dump.scala Thu Aug 29 15:43:05 2019 +0200
+++ b/src/Pure/Tools/dump.scala Thu Aug 29 17:13:49 2019 +0200
@@ -167,13 +167,22 @@
/* run session */
try {
+ val dump_checkpoint = deps.dump_checkpoint.toSet
+ def commit(snapshot: Document.Snapshot, status: Document_Status.Node_Status)
+ {
+ if (dump_checkpoint(snapshot.node_name)) {
+ session.protocol_command("ML_Heap.share_common_data")
+ }
+ Consumer.apply(snapshot, status)
+ }
+
val use_theories = resources.used_theories(deps).map(_.theory)
val use_theories_result =
session.use_theories(use_theories,
unicode_symbols = unicode_symbols,
share_common_data = true,
progress = progress,
- commit = Some(Consumer.apply _))
+ commit = Some(commit _))
val bad_theories = Consumer.shutdown()
val bad_msgs =