equal
deleted
inserted
replaced
295 resources: Resources, |
295 resources: Resources, |
296 reparse_limit: Int, |
296 reparse_limit: Int, |
297 previous: Document.Version, |
297 previous: Document.Version, |
298 doc_blobs: Document.Blobs, |
298 doc_blobs: Document.Blobs, |
299 edits: List[Document.Edit_Text], |
299 edits: List[Document.Edit_Text], |
300 consolidate: Boolean): Session.Change = |
300 consolidate: List[Document.Node.Name]): Session.Change = |
301 { |
301 { |
302 val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits) |
302 val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits) |
303 |
303 |
304 def get_blob(name: Document.Node.Name) = |
304 def get_blob(name: Document.Node.Name) = |
305 doc_blobs.get(name) orElse previous.nodes(name).get_blob |
305 doc_blobs.get(name) orElse previous.nodes(name).get_blob |