src/Pure/Thy/thy_syntax.scala
changeset 68336 09ac56914b29
parent 66772 a66f11a0b5b1
child 68381 2fd3a6d6ba2e
--- a/src/Pure/Thy/thy_syntax.scala	Thu May 31 22:10:06 2018 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu May 31 22:27:13 2018 +0200
@@ -296,7 +296,8 @@
       reparse_limit: Int,
       previous: Document.Version,
       doc_blobs: Document.Blobs,
-      edits: List[Document.Edit_Text]): Session.Change =
+      edits: List[Document.Edit_Text],
+      consolidate: Boolean): Session.Change =
   {
     val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
 
@@ -356,6 +357,7 @@
         (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes))
       }
 
-    Session.Change(previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, version)
+    Session.Change(
+      previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, consolidate, version)
   }
 }