src/Pure/Concurrent/future.ML
2013-03-05 wenzelm 2013-03-05 removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
2013-03-03 wenzelm 2013-03-03 more uniform Future.map: always internalize failure; added Future.flat as fast-path operation;
2013-02-26 wenzelm 2013-02-26 disallow shutdown from worker, which would lead to deadlock since the scheduler cannot terminate;
2013-02-26 wenzelm 2013-02-26 signal work_available should be sufficient to initiate daisy-chained workers, and lead to separate broadcast work_finished eventually -- NB: broadcasting all worker threads tends to burn parallel CPU cycles;
2013-02-26 wenzelm 2013-02-26 less eventful shutdown: merely wait for scheduler to terminate;
2013-02-26 wenzelm 2013-02-26 tuned messages;
2013-01-24 wenzelm 2013-01-24 report status more frequently on demand;
2013-01-19 wenzelm 2013-01-19 tuned signature;
2013-01-18 wenzelm 2013-01-18 more systematic task statistics;
2013-01-18 wenzelm 2013-01-18 added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
2013-01-17 wenzelm 2013-01-17 clarified Future.error_msg: slightly more robust id check, actually suppress displaced messages;
2013-01-16 wenzelm 2013-01-16 proper runtime position (cf. fe4714886d92 and Toplevel.error_msg) -- to make error messages actually appear in the document;
2013-01-16 wenzelm 2013-01-16 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16 wenzelm 2013-01-16 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2013-01-16 wenzelm 2013-01-16 tuned signature;
2013-01-02 wenzelm 2013-01-02 inline ML statistics into build log;
2013-01-01 wenzelm 2013-01-01 more robust report_status: tolerate ML_statistics even if ignored right now, e.g. in batch build;
2012-12-07 wenzelm 2012-12-07 final report_status within SYNCHRONIZED part of scheduler loop: required for sanity of data;
2012-11-29 wenzelm 2012-11-29 more uniform ML statistics;
2012-11-28 wenzelm 2012-11-28 some support for ML runtime statistics;
2012-10-19 wenzelm 2012-10-19 clarified Future.map (again): finished value is mapped in-place, which saves task structures and changes error behaviour slightly (tolerance against canceled group of old value etc.);
2012-10-18 wenzelm 2012-10-18 more uniform group for map_future, which is relevant for cancel in worker_task vs. future_job -- prefer peer group despite 81d03a29980c;
2012-10-18 wenzelm 2012-10-18 tuned comment;
2012-10-18 wenzelm 2012-10-18 more official Future.terminate; tuned signature;
2012-10-17 wenzelm 2012-10-17 more robust cancel_now: avoid shooting yourself in the foot;
2012-08-30 wenzelm 2012-08-30 refined status of forked goals;
2012-04-11 wenzelm 2012-04-11 more robust Future.fulfill wrt. duplicate assignment and interrupt;
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;