equal
deleted
inserted
replaced
259 case Interrupt_Prover => |
259 case Interrupt_Prover => |
260 if (prover != null) prover.interrupt |
260 if (prover != null) prover.interrupt |
261 |
261 |
262 case Edit_Version(edits) if prover != null => |
262 case Edit_Version(edits) if prover != null => |
263 val previous = global_state.peek().history.tip.version |
263 val previous = global_state.peek().history.tip.version |
264 val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) } |
264 val syntax = current_syntax() |
|
265 val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) } |
265 val change = global_state.change_yield(_.extend_history(previous, edits, result)) |
266 val change = global_state.change_yield(_.extend_history(previous, edits, result)) |
266 |
267 |
267 val this_actor = self |
268 val this_actor = self |
268 change.version.map(_ => { |
269 change.version.map(_ => { |
269 assignments.await { global_state.peek().is_assigned(previous.get_finished) } |
270 assignments.await { global_state.peek().is_assigned(previous.get_finished) } |