equal
deleted
inserted
replaced
49 previous: Document.Version, |
49 previous: Document.Version, |
50 syntax_changed: Boolean, |
50 syntax_changed: Boolean, |
51 deps_changed: Boolean, |
51 deps_changed: Boolean, |
52 doc_edits: List[Document.Edit_Command], |
52 doc_edits: List[Document.Edit_Command], |
53 version: Document.Version) |
53 version: Document.Version) |
|
54 |
|
55 case object Change_Flush |
54 |
56 |
55 |
57 |
56 /* events */ |
58 /* events */ |
57 |
59 |
58 //{{{ |
60 //{{{ |
318 { |
320 { |
319 private var postponed: List[Session.Change] = Nil |
321 private var postponed: List[Session.Change] = Nil |
320 |
322 |
321 def store(change: Session.Change): Unit = synchronized { postponed ::= change } |
323 def store(change: Session.Change): Unit = synchronized { postponed ::= change } |
322 |
324 |
323 def flush(): Unit = synchronized { |
325 def flush(state: Document.State): List[Session.Change] = synchronized { |
324 val state = global_state.value |
|
325 val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous)) |
326 val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous)) |
326 postponed = unassigned |
327 postponed = unassigned |
327 assigned.reverseIterator.foreach(change => manager.send(change)) |
328 assigned.reverse |
328 } |
329 } |
329 } |
330 } |
330 |
331 |
331 |
332 |
332 /* prover process */ |
333 /* prover process */ |
446 msg.text match { |
447 msg.text match { |
447 case Protocol.Assign_Update(id, update) => |
448 case Protocol.Assign_Update(id, update) => |
448 try { |
449 try { |
449 val cmds = global_state.change_result(_.assign(id, update)) |
450 val cmds = global_state.change_result(_.assign(id, update)) |
450 change_buffer.invoke(true, cmds) |
451 change_buffer.invoke(true, cmds) |
|
452 manager.send(Session.Change_Flush) |
451 } |
453 } |
452 catch { case _: Document.State.Fail => bad_output() } |
454 catch { case _: Document.State.Fail => bad_output() } |
453 postponed_changes.flush() |
|
454 case _ => bad_output() |
455 case _ => bad_output() |
455 } |
456 } |
456 delay_prune.invoke() |
457 delay_prune.invoke() |
457 |
458 |
458 case Markup.Removed_Versions => |
459 case Markup.Removed_Versions => |
459 msg.text match { |
460 msg.text match { |
460 case Protocol.Removed(removed) => |
461 case Protocol.Removed(removed) => |
461 try { |
462 try { |
462 global_state.change(_.removed_versions(removed)) |
463 global_state.change(_.removed_versions(removed)) |
|
464 manager.send(Session.Change_Flush) |
463 } |
465 } |
464 catch { case _: Document.State.Fail => bad_output() } |
466 catch { case _: Document.State.Fail => bad_output() } |
465 case _ => bad_output() |
467 case _ => bad_output() |
466 } |
468 } |
467 |
469 |
530 prover.get.terminate |
532 prover.get.terminate |
531 } |
533 } |
532 |
534 |
533 case Prune_History => |
535 case Prune_History => |
534 if (prover.defined) { |
536 if (prover.defined) { |
535 val old_versions = global_state.change_result(_.prune_history(prune_size)) |
537 val old_versions = global_state.change_result(_.remove_versions(prune_size)) |
536 if (!old_versions.isEmpty) prover.get.remove_versions(old_versions) |
538 if (!old_versions.isEmpty) prover.get.remove_versions(old_versions) |
537 } |
539 } |
538 |
540 |
539 case Update_Options(options) => |
541 case Update_Options(options) => |
540 if (prover.defined && is_ready) { |
542 if (prover.defined && is_ready) { |
555 |
557 |
556 case Protocol_Command(name, args) if prover.defined => |
558 case Protocol_Command(name, args) if prover.defined => |
557 prover.get.protocol_command(name, args:_*) |
559 prover.get.protocol_command(name, args:_*) |
558 |
560 |
559 case change: Session.Change if prover.defined => |
561 case change: Session.Change if prover.defined => |
560 if (global_state.value.is_assigned(change.previous)) |
562 val state = global_state.value |
|
563 if (!state.removing_versions && state.is_assigned(change.previous)) |
561 handle_change(change) |
564 handle_change(change) |
562 else postponed_changes.store(change) |
565 else postponed_changes.store(change) |
|
566 |
|
567 case Session.Change_Flush if prover.defined => |
|
568 val state = global_state.value |
|
569 if (!state.removing_versions) |
|
570 postponed_changes.flush(state).foreach(handle_change(_)) |
563 |
571 |
564 case bad => |
572 case bad => |
565 if (verbose) Output.warning("Ignoring bad message: " + bad.toString) |
573 if (verbose) Output.warning("Ignoring bad message: " + bad.toString) |
566 } |
574 } |
567 true |
575 true |