equal
deleted
inserted
replaced
234 } |
234 } |
235 recover(commands) |
235 recover(commands) |
236 } |
236 } |
237 |
237 |
238 edit match { |
238 edit match { |
239 case (_, Document.Node.Clear()) => node.clear |
|
240 |
|
241 case (_, Document.Node.Blob(blob)) => node.init_blob(blob) |
239 case (_, Document.Node.Blob(blob)) => node.init_blob(blob) |
242 |
240 |
243 case (name, Document.Node.Edits(text_edits)) => |
241 case (name, Document.Node.Edits(text_edits)) => |
244 if (name.is_theory) { |
242 if (name.is_theory) { |
245 val commands0 = node.commands |
243 val commands0 = node.commands |