--- a/src/Pure/PIDE/session.scala Mon Sep 30 17:28:40 2019 +0200
+++ b/src/Pure/PIDE/session.scala Mon Sep 30 21:01:08 2019 +0200
@@ -421,6 +421,10 @@
{
require(prover.defined)
+ if (change.share_common_data) {
+ prover.get.protocol_command("ML_Heap.share_common_data")
+ }
+
// define commands
{
val id_commands = new mutable.ListBuffer[Command]
@@ -453,9 +457,6 @@
val assignment = global_state.value.the_assignment(change.previous).check_finished
global_state.change(_.define_version(change.version, assignment))
- if (change.share_common_data) {
- prover.get.protocol_command("ML_Heap.share_common_data")
- }
prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate)
resources.commit(change)
}