Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin; TheoryView: simplified change_receiver, only for local purposes (via command_change); Accumulator: message requires explicit prover context for now;

tuned;

tuned;

Prover: just one actor -- single message dispatch; simplified states/commands/document_versions: immutable data;