pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;

cancel, shutdown: notify_all;

finish: Future.shutdown last;

eliminated requests, use global state variables uniformly; more robust shutdown;

finish: Future.shutdown;

added is_empty;

shutdown: global join-and-shutdown operation; reduced trace_active; scheduler_fork: always notify; tracing for thread exit; unique ids for workers;

added focus, which indicates a particular collection of high-priority tasks; tuned;

some general notes on future values;

separate Concurrent/ROOT.ML;

Parallel list combinators.

added Concurrent/par_list.ML;

added interrupt_task (external id); tuned signature;

tuned;

future_schedule: uninterruptible join;

added future_scheduler (default false);

replaced join_all by join_results, which returns Exn.results; join: disallow Multithreading.self_critical, which is prone to deadlocks due to context change via fork;

workers: explicit activity flag; SYNCHRONIZED: optional tracing;

future: allow explicit group; cancel: invalidate group identifier for all future members; tuned comments; tuned;

cancel: invalidate group implicitly, via bool ref; job: moved ok flag into group; added interrupt, interrupt_external for tasks;

auto_flush: uniform block buffering for all output streams;

auto_flush stdout, stderr as well;

proper values of no_interrupts, regular_interrupts;

cancel: check_scheduler; adapted to simplified TaskQueue.cancel; improved join/join_all: actively work towards results, i.e. do not yield unnecessarily; misc tuning;

simplified dequeue: provide Thread.self internally; simplified cancel: interrupt running threads internally; added depend; added dequeue_towards; misc tuning;

eliminated cache, access queue efficiently via IntGraph.get_first;

export get_first from underlying table;

out_stream: block-buffered, with separate autoflush thread (every 50ms);

babel: removed unnecessary "french" option, which actually enables french section names etc. on some LaTeX installations;

added comment

human-readable printing of TaskQueue.task/group;

* Changed defaults for unify configuration options;

inherit group from running thread, or create a new one -- make it harder to re-use canceled groups; group is now non-optional; tuned signature; replaced low-level interrupts by group cancel operation; misc tuning;

job: explicit 'ok' status -- false for canceled jobs; group is now non-optional; tuned signature; replaced low-level interrupts by group cancel operation; misc tuning;

Overall exception handler in order to insulate our users from low-level bugs.

more careful exception handling in order to prevent backtracking; miscellaneous tidying up.

Increasing the default limits in order to prevent unnecessary failures.

send: broadcast condition while locked!

proper signature constraint;

tuned Mailbox.send;

removed unused sync_interrupts;

moved thread data to future.ML (again); dequeue: include group; more interrupt operations; misc tuning;

more interrupt operations; maintain thread data (formerly in task_queue.ML); wait: added tracing; added requests mailbox; handle excessive workers fork: inherit group; added rudimentary shutdown; misc tuning;

moved task, thread_data, group, queue to task_queue.ML; tuned signature; SYNCHRONIZED notify_all! misc tuning;

Ordered queue of grouped tasks. formerly in future.ML; added thread data; added group; more robust dequeue: change into running here; misc tuning;

added Concurrent/task_queue.ML;

await: SYNCHRONIZED wait!

tuned check_cache; removed broken self_synchronized, which cannot be used in conjunction with condition variables; more precise use of SYNCHRONIZED vs. wait; tuned worker_loop;

added sync_interrupts, regular_interrupts; max_thread_value: enforce >= 1;

added sync_interrupts, regular_interrupts;

opaque signature constraint abstracts local type abbrev;

tuned;

added change_result;

Functional threads as future values.

added Concurrent/future.ML;

Default (mostly dummy) implementation of thread structures. formerly in multithreading.ML; create mutexes / condition variables without failure;

*** MESSAGE REFERS TO PREVIOUS VERSION *** removed dummy thread structures from multithreading.ML;

*** empty log message ***

explicit use of universal.ML and dummy_thread.ML;

added no_interrupts; tuned;