future_job: more robust Exn.capture outside thread attribute change;

shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;

future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group; control combinators: paranoia eta-expansion to ensure proper operational semantics;

maintain Future.worker_group as management data; cancel_thy: refer to proper task group; tuned;

join_proofs: implicit exception; removed obsolete cancel_proofs, cf. cancel_thy in thy_info.ML; tuned;

simultaneous join_proofs; removed obsolete promises_of;

map: subgroup of worker_group;

added worker_group; fork: default to subgroup of worker_group; removed obsolete fork_local; join/get_result: cumulative flattened exceptions; map: subgroup of worker_group;

support for nested groups -- cancellation is propagated to peers and subgroups; added is_canceled; tuned;

added flatten/flatten_list -- supercedes internal plain_exns; represent empty failure as EXCEPTIONS [] instead of Interrupt;

propagate exceptions within future groups; Future.map: inherit group;

less ambitious ML_OPTIONS;

disabled macbroy6 -- hardware repair;

tuned;

tuned tracing; provide spare worker threads to saturate hardware while other workers wait during join;

prefer simultaneous join -- for improved scheduling;

tuned dequeu_towards: try immediate tasks before expensive all_preds;

Display.pretty_thm now requires a proper context;

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

moved ProofContext.pretty_thm to Display.pretty_thm etc.; explicit old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.; removed some very old thm print operations;

moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;

removed obsolete CVS Ids;

merged

merged

deftab: only process theorems on demand

no SAME exceptions in uncritical code

merged

less digestible

refined outline structure

replaced usedir option -Q by more fine-grained -q;

merged

merged