clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;

tuned whitespace;

more toplevel pretty printing;

back to full synchronization (cf. eb3e399f5b9f);

proper sequential version;

eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer); clarified Command.run_process etc.: join running eval, bypass running print; eliminated Command.memo in favour of regular Lazy.lazy; more Lazy.lazy status information;

modernized historic example;

more thorough Lazy.is_finished;

3 old example lemmas by Amine listed in the top 100 theorems

update_cartouches; trimmed whitespace;

memo_fork without locking, to avoid rare deadlock in Event_Timer.request due to execution overrun;

typos

unused;

tuned message;

explicit message channels for "state", "information"; separate state_message_color;

imitate font more carefully: err on smaller size; imitate HTML font, notably for Sidekick where short string is also shown as view status message;