scheduler: shutdown spontaneously (after some delay) if queue is empty; scheduler_check: critical, only performed after fork/enqueue; shutdown: passively wait for termination;

join_next: do not yield, even if overloaded, to minimize "running" tasks;

tuned tracing;

cancel: improved reactivity due to more careful broadcasting; internal broadcast_all;

dequeue_towards: always return active tasks; join_work: imitate worker more closely, keep active if queue appears to be blocked for the moment -- it may become free again after some worker_finished event;

merged

removed unused low-level interrupts;

tuned signature;

tuned;

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;

enqueue/finish: return minimal/maximal state of this task;

NEWS

tacticals FOCUS and FOCUS_PARAMS;

replaced old METAHYPS by FOCUS; eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body; modernized functor names; minimal tuning of sources; reactivated dead quasi.ML (ever used?);

replaced old METAHYPS by FOCUS;

added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;

replaced old METAHYPS by FOCUS;

tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);

retrofit: actually handle schematic variables -- need to export into original context;

merged

adapted to changed prefixes

merged

improved handling of parameter import; tuned

explicit is better than implicit