equal
deleted
inserted
replaced
134 name: Document.Node.Name, text_perspective: Text.Perspective) |
134 name: Document.Node.Name, text_perspective: Text.Perspective) |
135 : (Command.Perspective, Document.Version) = |
135 : (Command.Perspective, Document.Version) = |
136 { |
136 { |
137 val nodes = previous.nodes |
137 val nodes = previous.nodes |
138 val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective) |
138 val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective) |
139 val version = Document.Version.make(new_nodes getOrElse nodes) |
139 val version = Document.Version.make(previous.syntax, new_nodes getOrElse nodes) |
140 (perspective, version) |
140 (perspective, version) |
141 } |
141 } |
142 |
142 |
143 |
143 |
144 |
144 |
263 case (perspective, Some(nodes1)) => |
263 case (perspective, Some(nodes1)) => |
264 doc_edits += (name -> Document.Node.Perspective(perspective)) |
264 doc_edits += (name -> Document.Node.Perspective(perspective)) |
265 nodes = nodes1 |
265 nodes = nodes1 |
266 } |
266 } |
267 } |
267 } |
268 (doc_edits.toList, Document.Version.make(nodes)) |
268 (doc_edits.toList, Document.Version.make(syntax, nodes)) |
269 } |
269 } |
270 } |
270 } |
271 } |
271 } |