--- a/src/Pure/Thy/thy_syntax.scala Wed Aug 28 10:18:50 2019 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Aug 28 22:59:49 2019 +0200
@@ -297,7 +297,8 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text],
- consolidate: List[Document.Node.Name]): Session.Change =
+ consolidate: List[Document.Node.Name],
+ share_common_data: Boolean): Session.Change =
{
val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
@@ -358,6 +359,7 @@
}
Session.Change(
- previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, consolidate, version)
+ previous, syntax_changed, syntax_changed.nonEmpty, doc_edits,
+ consolidate, share_common_data, version)
}
}