equal
deleted
inserted
replaced
519 } |
519 } |
520 finished = true |
520 finished = true |
521 receiver.cancel() |
521 receiver.cancel() |
522 reply(()) |
522 reply(()) |
523 |
523 |
524 case Update_Options(options) if prover.isDefined => |
524 case Update_Options(options) => |
525 if (is_ready) { |
525 if (prover.isDefined && is_ready) { |
526 prover.get.options(options) |
526 prover.get.options(options) |
527 handle_raw_edits(Document.Blobs.empty, Nil) |
527 handle_raw_edits(Document.Blobs.empty, Nil) |
528 } |
528 } |
529 global_options.event(Session.Global_Options(options)) |
529 global_options.event(Session.Global_Options(options)) |
530 reply(()) |
530 reply(()) |