293 } |
293 } |
294 } |
294 } |
295 |
295 |
296 def parse_change( |
296 def parse_change( |
297 session: Session, |
297 session: Session, |
298 reparse_limit: Int, |
|
299 previous: Document.Version, |
298 previous: Document.Version, |
300 doc_blobs: Document.Blobs, |
299 doc_blobs: Document.Blobs, |
301 edits: List[Document.Edit_Text], |
300 edits: List[Document.Edit_Text], |
302 consolidate: List[Document.Node.Name] |
301 consolidate: List[Document.Node.Name] |
303 ): Session.Change = { |
302 ): Session.Change = { |
304 val resources = session.resources |
303 val resources = session.resources |
305 val session_base = resources.session_base |
304 val session_base = resources.session_base |
|
305 val reparse_limit = session.reparse_limit |
306 |
306 |
307 val (syntax_changed, nodes0, doc_edits0) = header_edits(session_base, previous, edits) |
307 val (syntax_changed, nodes0, doc_edits0) = header_edits(session_base, previous, edits) |
308 |
308 |
309 def get_blob(name: Document.Node.Name): Option[Document.Blobs.Item] = |
309 def get_blob(name: Document.Node.Name): Option[Document.Blobs.Item] = |
310 doc_blobs.get(name) orElse previous.nodes(name).get_blob |
310 doc_blobs.get(name) orElse previous.nodes(name).get_blob |