equal
deleted
inserted
replaced
211 |
211 |
212 val text_edits: List[Document.Edit_Text] = |
212 val text_edits: List[Document.Edit_Text] = |
213 List((name, Document.Node.Perspective(text_perspective))) |
213 List((name, Document.Node.Perspective(text_perspective))) |
214 val change = |
214 val change = |
215 global_state.change_yield( |
215 global_state.change_yield( |
216 _.extend_history(Future.value(previous), text_edits, Future.value(version))) |
216 _.continue_history(Future.value(previous), text_edits, Future.value(version))) |
217 |
217 |
218 val assignment = global_state().the_assignment(previous).get_finished |
218 val assignment = global_state().the_assignment(previous).get_finished |
219 global_state.change(_.define_version(version, assignment)) |
219 global_state.change(_.define_version(version, assignment)) |
220 global_state.change_yield(_.assign(version.id, Nil)) |
220 global_state.change_yield(_.assign(version.id, Nil)) |
221 |
221 |
233 val previous = global_state().history.tip.version |
233 val previous = global_state().history.tip.version |
234 |
234 |
235 val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit)) |
235 val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit)) |
236 val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) } |
236 val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) } |
237 val change = |
237 val change = |
238 global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2))) |
238 global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2))) |
239 |
239 |
240 result.map { |
240 result.map { |
241 case (doc_edits, _) => |
241 case (doc_edits, _) => |
242 assignments.await { global_state().is_assigned(previous.get_finished) } |
242 assignments.await { global_state().is_assigned(previous.get_finished) } |
243 this_actor ! Change_Node(name, doc_edits, previous.join, change.version.join) |
243 this_actor ! Change_Node(name, doc_edits, previous.join, change.version.join) |