equal
deleted
inserted
replaced
294 def parse_change( |
294 def parse_change( |
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]): Session.Change = |
299 edits: List[Document.Edit_Text], |
|
300 consolidate: Boolean): Session.Change = |
300 { |
301 { |
301 val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits) |
302 val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits) |
302 |
303 |
303 def get_blob(name: Document.Node.Name) = |
304 def get_blob(name: Document.Node.Name) = |
304 doc_blobs.get(name) orElse previous.nodes(name).get_blob |
305 doc_blobs.get(name) orElse previous.nodes(name).get_blob |
354 nodes += (name -> node3) |
355 nodes += (name -> node3) |
355 } |
356 } |
356 (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes)) |
357 (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes)) |
357 } |
358 } |
358 |
359 |
359 Session.Change(previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, version) |
360 Session.Change( |
|
361 previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, consolidate, version) |
360 } |
362 } |
361 } |
363 } |