diff -r 2f080a51a10d -r 09ac56914b29 src/Pure/PIDE/resources.scala --- 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) { }