src/Pure/PIDE/resources.scala
changeset 68336 09ac56914b29
parent 68317 938803796a8b
child 68381 2fd3a6d6ba2e
--- a/src/Pure/PIDE/resources.scala	Thu May 31 22:10:06 2018 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu May 31 22:27:13 2018 +0200
@@ -215,8 +215,9 @@
       reparse_limit: Int,
       previous: Document.Version,
       doc_blobs: Document.Blobs,
-      edits: List[Document.Edit_Text]): Session.Change =
-    Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits)
+      edits: List[Document.Edit_Text],
+      consolidate: Boolean): Session.Change =
+    Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
 
   def commit(change: Session.Change) { }