src/Pure/Concurrent/future.ML
2012-04-11 wenzelm 2012-04-11 always signal after cancel_group: passive tasks may have become active;
2012-04-09 wenzelm 2012-04-09 simplified Future.cancel/cancel_group (again) -- running threads only; more robust update/cancel_execution: full join_tasks of group before exec state assignment; tuned signature;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-10-13 wenzelm 2011-10-13 static dummy_task (again) to avoid a few extra allocations;
2011-08-23 wenzelm 2011-08-23 tuned signature;
2011-08-23 wenzelm 2011-08-23 discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);
2011-08-23 wenzelm 2011-08-23 some support for toplevel printing wrt. editor perspective (still inactive);
2011-08-21 wenzelm 2011-08-21 purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;
2011-08-20 wenzelm 2011-08-20 added Future.joins convenience; clarified Future.map: based on Future.cond_forks;
2011-08-19 wenzelm 2011-08-19 tuned signature (again); tuned;
2011-08-19 wenzelm 2011-08-19 tuned signature -- treat structure Task_Queue as private to implementation;
2011-08-19 wenzelm 2011-08-19 refined Future.cancel: explicit future allows to join actual cancellation; Document.cancel_execution: join nested future groups as well;
2011-08-19 wenzelm 2011-08-19 Future.promise: explicit abort operation (like uninterruptible future job); explicit cancel_scala message -- still unused;
2011-08-19 wenzelm 2011-08-19 more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
2011-08-19 wenzelm 2011-08-19 clarified Future.cond_forks: more uniform handling of exceptional situations;
2011-08-18 wenzelm 2011-08-18 tuned comments;
2011-08-17 wenzelm 2011-08-17 identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
2011-08-17 wenzelm 2011-08-17 more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;
2011-08-15 wenzelm 2011-08-15 explicit check of finished evaluation;
2011-08-13 wenzelm 2011-08-13 immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029); more careful treatment of last_round on startup/shutdown;
2011-08-10 wenzelm 2011-08-10 tuned signature;
2011-08-10 wenzelm 2011-08-10 future_job: explicit indication of interrupts;
2011-08-10 wenzelm 2011-08-10 synchronized cancel and flushing of Multithreading.interrupted state, to ensure that interrupts stay within task boundaries;
2011-08-10 wenzelm 2011-08-10 tuned source structure;
2011-07-23 wenzelm 2011-07-23 make double-sure that interrupts are flushed before executing new work (cf. 22f8c2483bd2);
2011-07-23 wenzelm 2011-07-23 more detailed tracing; tuned;
2011-07-11 wenzelm 2011-07-11 tuned signature -- corresponding to Scala version;
2011-07-05 wenzelm 2011-07-05 tuned signature; tuned;
2011-06-23 wenzelm 2011-06-23 more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
2011-03-26 wenzelm 2011-03-26 added Future.cond_forks convenience;
2011-02-18 wenzelm 2011-02-18 less verbose tracing;
2011-02-09 wenzelm 2011-02-09 tuned scope of Multithreading.interrupted vs. Multithreading.with_attributes;
2011-02-08 wenzelm 2011-02-08 explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;
2011-02-04 wenzelm 2011-02-04 tuned signature; tuned;
2011-02-02 wenzelm 2011-02-02 eliminated slightly odd abstract type Task_Queue.deps; tuned signature; tuned;
2011-02-02 wenzelm 2011-02-02 maintain Task_Queue.group within Task_Queue.task; Task_Queue.dummy_task: id = 0 in accordance to Document.no_id etc.; tuned signature;
2011-02-02 wenzelm 2011-02-02 Future.join_results: discontinued post-hoc recording of dynamic dependencies; abstract Task_Queue.deps; tuned signature; tuned;
2011-02-01 wenzelm 2011-02-01 more informative task timing: some dependency tracking;
2011-02-01 wenzelm 2011-02-01 refined task timing: joining vs. waiting; tuned;
2011-01-31 wenzelm 2011-01-31 tuned signature; tuned vacous forks;
2011-01-31 wenzelm 2011-01-31 support named tasks, for improved tracing;
2011-01-31 wenzelm 2011-01-31 more direct Future.bulk, which potentially reduces overhead for Par_List; tuned signature;
2011-01-31 wenzelm 2011-01-31 added basic task timing;
2010-11-09 wenzelm 2010-11-09 explicitly identify forked/joined tasks;
2010-11-02 wenzelm 2010-11-02 simplified some time constants;
2010-09-10 wenzelm 2010-09-10 Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
2010-09-09 wenzelm 2010-09-09 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-08-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-07-22 wenzelm 2010-07-22 tuned comments;
2010-07-21 wenzelm 2010-07-21 clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
2010-07-20 wenzelm 2010-07-20 back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c); cancel passive tasks more actively via Exn.Interrupt, by treating them like ragular jobs here; attempts to re-assign canceled futures/promises raise Exn.Interrupt; tuned;
2010-07-20 wenzelm 2010-07-20 eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that; tuned some error messages;
2010-07-04 wenzelm 2010-07-04 general Future.report -- also for Toplevel.async_state;
2010-07-02 wenzelm 2010-07-02 tuned white space;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-29 wenzelm 2010-05-29 future result: retain plain Interrupt for vacuous group exceptions;
2010-05-21 wenzelm 2010-05-21 future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);
2010-02-06 wenzelm 2010-02-06 result: Single_Assignment.var;
2010-01-06 wenzelm 2010-01-06 more robust cancelation, notably of passive futures without scheduler running;
2010-01-06 wenzelm 2010-01-06 eliminated cache, which complicates the code without making a real difference (NB: deque_towards often disrupts caching, and daisy-chaining of workers already reduces queue overhead);