405 node: Document.Node, edit: Document.Edit_Text): Document.Node = |
405 node: Document.Node, edit: Document.Edit_Text): Document.Node = |
406 { |
406 { |
407 edit match { |
407 edit match { |
408 case (_, Document.Node.Clear()) => node.clear |
408 case (_, Document.Node.Clear()) => node.clear |
409 |
409 |
410 case (_, Document.Node.Blob()) => node |
410 case (_, Document.Node.Blob()) => node.init_blob |
411 |
411 |
412 case (name, Document.Node.Edits(text_edits)) => |
412 case (name, Document.Node.Edits(text_edits)) => |
413 val commands0 = node.commands |
413 if (node.is_blob) node |
414 val commands1 = edit_text(text_edits, commands0) |
414 else { |
415 val commands2 = |
415 val commands0 = node.commands |
416 recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1) |
416 val commands1 = edit_text(text_edits, commands0) |
417 node.update_commands(commands2) |
417 val commands2 = |
|
418 recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1) |
|
419 node.update_commands(commands2) |
|
420 } |
418 |
421 |
419 case (_, Document.Node.Deps(_)) => node |
422 case (_, Document.Node.Deps(_)) => node |
420 |
423 |
421 case (name, Document.Node.Perspective(required, text_perspective, overlays)) => |
424 case (name, Document.Node.Perspective(required, text_perspective, overlays)) => |
422 val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays) |
425 val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays) |