more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
more specific signal vs. broadcast;
execute/finish: more careful notification based on minimal/maximal status;
tuned shutdown;
set ThyOutput.source;
use "../../antiquote_setup.ML";
use_thy "Basics";
use_thy "Interfaces";
use_thy "Presentation";
use_thy "Misc";