changeset 68381 | 2fd3a6d6ba2e |
parent 68336 | 09ac56914b29 |
child 68762 | 8750edd967ce |
--- a/src/Pure/PIDE/resources.scala Tue Jun 05 14:15:49 2018 +0200 +++ b/src/Pure/PIDE/resources.scala Tue Jun 05 16:12:26 2018 +0200 @@ -216,7 +216,7 @@ previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text], - consolidate: Boolean): Session.Change = + consolidate: List[Document.Node.Name]): Session.Change = Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate) def commit(change: Session.Change) { }