src/Pure/Concurrent/par_exn.ML
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;
2012-09-01 wenzelm 2012-09-01 central management of forked goals wrt. transaction id; clarified stable_exec_id: consider ragular failure as stable; more robust counting of forked proofs, with global reset after cancellation due to document editing;
2012-04-04 wenzelm 2012-04-04 proper signature constraint;
2011-08-20 wenzelm 2011-08-20 more direct balanced version Ord_List.unions;
2011-08-19 wenzelm 2011-08-19 more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
2011-08-18 wenzelm 2011-08-18 more precise treatment of exception nesting and serial numbers;
2011-08-18 wenzelm 2011-08-18 more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-18 wenzelm 2011-08-18 clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
2011-08-18 wenzelm 2011-08-18 tune Par_Exn.make: balance merge; clarified Par_Exn.dest: later exceptions first;
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 clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
2011-08-17 wenzelm 2011-08-17 more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;