basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

load underscore package after iman etc.;

tuned comment;

added formal markup for setting, executable, tool;

basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

converted basics.tex to theory file;

added isatt markup;

New outline for codegen tutorial -- draft

added extern_fact (local or global); more procise printing of fact names;

print raw (internal) result names;

more procise printing of fact names;

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;

added no_interrupts; moved dummy thread structures to dummy_thread.ML;

tuned;

send: broadcast to all waiting threads;

added ML-Systems/thread_dummy.ML;

dropped "run" marker in monad syntax

multithreading.ML provides dummy thread structures;

different bookkeeping for code equations

renamed structure CodeTarget to Code_Target

instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel

proper header;

added receive_timeout; tuned comments;

check WRAPPER_OUTPUT node type;

init: disallow "" as out stream;

fixed deps: no Concurrent/receiver.ML yet;

Concurrent message exchange via mailbox -- with unbounded queueing.

added Concurrent/mailbox.ML;

reorganize subsections

rename INF_drop_prefix to INFM_drop_prefix

add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1

move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add

tuned signature;

added General/queue.ML;

Efficient queues.

moved Multithreading.task/schedule to Concurrent/schedule.ML

multithreading.ML provides dummy thread structures;