src/Pure/context.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-03-21 wenzelm 2009-03-21 removed obsolete pprint operations; some explicit pp operations for toplevel pretty printing;
2009-01-06 wenzelm 2009-01-06 renamed structure ParList to Par_List;
2009-01-06 wenzelm 2009-01-06 parallelized merge_data;
2008-12-13 wenzelm 2008-12-13 tuned comments; tuned;
2008-12-13 wenzelm 2008-12-13 refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry; tuned history: renamed version to stage, disallow checkpoint/finish_thy on finished theories; added display_names -- user-level presentation; removed obsolete exists_name, names_of; tuned;
2008-12-11 wenzelm 2008-12-11 unified ids for ancestors and checkpoints, removed obsolete history of checkpoints; tuned representation of internal node names -- avoid string copies; tuned signature;
2008-12-06 wenzelm 2008-12-06 finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
2008-10-16 wenzelm 2008-10-16 tuned;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-22 wenzelm 2008-09-22 added reject_draft;
2008-09-04 wenzelm 2008-09-04 Thread.getLocal/setLocal;
2008-06-24 wenzelm 2008-06-24 added pprint_thy_ref;
2008-05-18 wenzelm 2008-05-18 eliminated theory CPure;
2008-05-14 wenzelm 2008-05-14 names_of: exclude intermediate ids -- less verbosity;
2008-04-10 wenzelm 2008-04-10 export is_draft, not draftN;
2008-03-29 wenzelm 2008-03-29 added map_theory_result, map_proof_result;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure; implicit setup of emerging theory Pure; added >>> operator;
2008-03-27 wenzelm 2008-03-27 nonfix >>;
2008-03-26 wenzelm 2008-03-26 added thread data (formerly global ref in ML/ml_context.ML); renamed ML_Context.>> to Context.>> (again);
2007-09-08 wenzelm 2007-09-08 removed thy_ord (erratic due to multi-threading);
2007-08-20 wenzelm 2007-08-20 tuned CRITICAL sections;
2007-08-08 wenzelm 2007-08-08 thread-safeness: when creating certified items, perform Theory.check_thy *last*; tuned datatype proof;
2007-08-03 wenzelm 2007-08-03 improved check_thy: produce a checked theory_ref (thread-safe version); removed obsolete self_ref (cf. check_thy); thread-safeness: when creating certified items, perform Theory.check_thy *last*; eq_thy: no check here; marked some critical sections;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections;
2007-07-05 wenzelm 2007-07-05 the_theory/proof: error instead of exception Fail;
2007-06-13 wenzelm 2007-06-13 merge/merge_refs: plain error instead of exception TERM;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
2007-04-30 wenzelm 2007-04-30 removed obsolete get_sg;
2007-04-05 wenzelm 2007-04-05 added thy_ord -- order of creation; ancestors: back to traditional ad-hoc order (avoid occasional problems with get_thm);
2007-04-04 wenzelm 2007-04-04 theory: maintain ancestors in order of creation;
2007-01-21 wenzelm 2007-01-21 *** MESSAGE REFERS TO PREVIOUS VERSION *** removed is_finished_thy;
2007-01-21 wenzelm 2007-01-21 tuned comments
2007-01-20 wenzelm 2007-01-20 added is_finished_thy;
2007-01-19 wenzelm 2007-01-19 moved ML context stuff to from Context to ML_Context;
2007-01-19 wenzelm 2007-01-19 ML context: full generic context, tuned signature;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-05 wenzelm 2006-12-05 added mapping_result;
2006-11-24 wenzelm 2006-11-24 fake predeclaration of structure ProofContext;
2006-10-09 wenzelm 2006-10-09 moved Context.ml_output to Output.ml_output;
2006-10-01 wenzelm 2006-10-01 exists_name: include this theory name;
2006-08-02 wenzelm 2006-08-02 fake predeclaration of type Proof.context;
2006-06-07 haftmann 2006-06-07 fixed typo
2006-05-17 wenzelm 2006-05-17 added mapping;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-12 wenzelm 2006-02-12 structure Datatab: private copy avoids potential conflict of table exceptions; simplified TableFun.join;
2006-02-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list;
2006-01-21 wenzelm 2006-01-21 rename map_theory/proof to theory/proof_map; added separate map_theory/proof;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory; use_output: Output.ML_errors;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-13 wenzelm 2006-01-13 added map_theory, map_proof;
2006-01-10 wenzelm 2006-01-10 support for generic contexts with data;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-13 wenzelm 2005-09-13 replaced DATA_FAIL by EXCEPTION;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;