more robust prover termination;

more explicit checks;

tuned signature;

more uniform warning/error handling, potentially with propagation to send_wait caller;

more careful shutdown (amending f2f53f7046f4);

misc tuning;

obsolete;

converted main session manager to Consumer_Thread: messages need to be consumed immediately, postponed_changes replaces implicit actor mailbox scanning;

simplified commands_changed_buffer (in contrast to a8331fb5c959): rely on better performance of Consumer_Thread/Mailbox and more direct Timer (like session_actor.receiver);

simplified -- prefer Consumer_Thread over Actor;

tuned imports;

support for requests with explicit acknowledgment (and exception propagation);

more robust thread: continue after failure;

clarified command_input: Consumer_Thread;

further robustification wrt. unclear ranges;

allow more control of main loop; more robust is_active test, although thread could terminate at any time;

eliminated pointless output actors; clarified command_input, which already includes thread.join;

more robust shutdown; less ooddities;

consumer thread with unbounded queueing of requests (similar to Message_Channel in ML);

proper signaling after each state update (NB: ML version does this uniformly via timed_access);

added Mailbox, as in ML;

synchronized access, similar to ML version;

tuned signature, in accordance to ML version;

eliminated redundant Volatile;

retain canonical reverse order;

more canonical list operations;

tuned signature in accordance to ML version;

canonical list operations, as in ML; avoid odd mutable data structures;

more uniform synchronized variables;

more unfolding and more folding in size equations, to look more natural in the nested case