2008-09-16 haftmann 2008-09-16 generic value command
2008-09-15 wenzelm 2008-09-15 converted symbols.tex;
2008-09-15 wenzelm 2008-09-15 tuned;
2008-09-15 wenzelm 2008-09-15 converted misc.tex;
2008-09-15 wenzelm 2008-09-15 tuned;
2008-09-15 wenzelm 2008-09-15 generated files;
2008-09-15 wenzelm 2008-09-15 converted present.tex;
2008-09-15 wenzelm 2008-09-15 basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
2008-09-15 wenzelm 2008-09-15 load underscore package after iman etc.;
2008-09-15 wenzelm 2008-09-15 tuned comment;
2008-09-15 wenzelm 2008-09-15 added formal markup for setting, executable, tool;
2008-09-15 wenzelm 2008-09-15 basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
2008-09-15 wenzelm 2008-09-15 converted basics.tex to theory file;
2008-09-15 wenzelm 2008-09-15 added isatt markup;
2008-09-14 haftmann 2008-09-14 New outline for codegen tutorial -- draft
2008-09-12 wenzelm 2008-09-12 added extern_fact (local or global); more procise printing of fact names;
2008-09-12 wenzelm 2008-09-12 print raw (internal) result names;
2008-09-12 wenzelm 2008-09-12 more procise printing of fact names;
2008-09-12 wenzelm 2008-09-12 pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
2008-09-11 wenzelm 2008-09-11 cancel, shutdown: notify_all;
2008-09-11 wenzelm 2008-09-11 finish: Future.shutdown last;
2008-09-11 wenzelm 2008-09-11 eliminated requests, use global state variables uniformly; more robust shutdown;
2008-09-11 wenzelm 2008-09-11 finish: Future.shutdown;
2008-09-11 wenzelm 2008-09-11 added is_empty;
2008-09-11 wenzelm 2008-09-11 shutdown: global join-and-shutdown operation; reduced trace_active; scheduler_fork: always notify; tracing for thread exit; unique ids for workers;
2008-09-11 wenzelm 2008-09-11 added focus, which indicates a particular collection of high-priority tasks; tuned;
2008-09-11 wenzelm 2008-09-11 some general notes on future values;
2008-09-11 wenzelm 2008-09-11 separate Concurrent/ROOT.ML;
2008-09-11 wenzelm 2008-09-11 Parallel list combinators.
2008-09-11 wenzelm 2008-09-11 added Concurrent/par_list.ML;
2008-09-10 wenzelm 2008-09-10 added interrupt_task (external id); tuned signature;
2008-09-10 wenzelm 2008-09-10 tuned;
2008-09-10 wenzelm 2008-09-10 future_schedule: uninterruptible join;
2008-09-10 wenzelm 2008-09-10 added future_scheduler (default false);
2008-09-10 wenzelm 2008-09-10 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;
2008-09-10 wenzelm 2008-09-10 workers: explicit activity flag; SYNCHRONIZED: optional tracing;
2008-09-10 wenzelm 2008-09-10 future: allow explicit group; cancel: invalidate group identifier for all future members; tuned comments; tuned;
2008-09-10 wenzelm 2008-09-10 cancel: invalidate group implicitly, via bool ref; job: moved ok flag into group; added interrupt, interrupt_external for tasks;
2008-09-10 wenzelm 2008-09-10 auto_flush: uniform block buffering for all output streams;
2008-09-09 wenzelm 2008-09-09 auto_flush stdout, stderr as well;
2008-09-09 wenzelm 2008-09-09 proper values of no_interrupts, regular_interrupts;
2008-09-09 wenzelm 2008-09-09 cancel: check_scheduler; adapted to simplified TaskQueue.cancel; improved join/join_all: actively work towards results, i.e. do not yield unnecessarily; misc tuning;
2008-09-09 wenzelm 2008-09-09 simplified dequeue: provide Thread.self internally; simplified cancel: interrupt running threads internally; added depend; added dequeue_towards; misc tuning;
2008-09-09 wenzelm 2008-09-09 eliminated cache, access queue efficiently via IntGraph.get_first;
2008-09-09 wenzelm 2008-09-09 export get_first from underlying table;
2008-09-09 wenzelm 2008-09-09 out_stream: block-buffered, with separate autoflush thread (every 50ms);
2008-09-09 wenzelm 2008-09-09 babel: removed unnecessary "french" option, which actually enables french section names etc. on some LaTeX installations;
2008-09-09 nipkow 2008-09-09 added comment
2008-09-09 wenzelm 2008-09-09 human-readable printing of TaskQueue.task/group;
2008-09-09 wenzelm 2008-09-09 * Changed defaults for unify configuration options;
2008-09-09 wenzelm 2008-09-09 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;
2008-09-09 wenzelm 2008-09-09 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;
2008-09-09 paulson 2008-09-09 Overall exception handler in order to insulate our users from low-level bugs.
2008-09-09 paulson 2008-09-09 more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
2008-09-09 paulson 2008-09-09 Increasing the default limits in order to prevent unnecessary failures.
2008-09-08 wenzelm 2008-09-08 send: broadcast condition while locked!
2008-09-08 wenzelm 2008-09-08 proper signature constraint;
2008-09-08 wenzelm 2008-09-08 tuned Mailbox.send;
2008-09-08 wenzelm 2008-09-08 removed unused sync_interrupts;
2008-09-08 wenzelm 2008-09-08 moved thread data to future.ML (again); dequeue: include group; more interrupt operations; misc tuning;