tuned;

added lemma

typo

avoid writing into source

clarified active_job: take dependencies into account (e.g. future based on promise);

tuned;

non-strict print_state: display old proof state on failure, e.g. unfinished command;

permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;

clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;

ignore print process even after fork, to avoid loosing active worker threads;