src/Pure/context.ML
2012-12-08 ago check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);
2012-08-29 ago renamed Position.str_of to Position.here;
2012-08-01 ago more standard bootstrapping of Pure.thy;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2011-07-06 ago prefer Synchronized.var;
2011-06-30 ago back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
2011-05-15 ago timing of Theory_Data operations, with implicit thread positions when functor is applied;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-16 ago modernized structure Proof_Context;
2011-02-05 ago more tracing information via Par_List.map_name;
2010-09-01 ago replaced Table.map' by Table.map
2010-07-21 ago replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
2010-07-21 ago added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
2010-07-20 ago 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;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-01-04 ago discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
2010-01-04 ago removed further remains of mutable theory data (cf. 25bd3ed2ac9f);
2010-01-04 ago dropped copy operation for legacy TheoryDataFun
2009-11-11 ago local mutex for theory content/identity operations;
2009-11-08 ago modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
2009-10-20 ago tuned;
2009-10-20 ago backpatching of structure Proof and ProofContext -- avoid odd aliases;
2009-09-30 ago eliminated redundant bindings;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-09 ago renamed functor TableFun to Table, and GraphFun to Graph;
2009-03-21 ago removed obsolete pprint operations;
2009-01-06 ago renamed structure ParList to Par_List;
2009-01-06 ago parallelized merge_data;
2008-12-13 ago tuned comments;
2008-12-13 ago refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
2008-12-11 ago unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
2008-12-06 ago 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 ago tuned;
2008-09-26 ago eliminated polymorphic equality;
2008-09-22 ago added reject_draft;
2008-09-04 ago Thread.getLocal/setLocal;
2008-06-24 ago added pprint_thy_ref;
2008-05-18 ago eliminated theory CPure;
2008-05-14 ago names_of: exclude intermediate ids -- less verbosity;
2008-04-10 ago export is_draft, not draftN;
2008-03-29 ago added map_theory_result, map_proof_result;
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2008-03-27 ago eliminated theory ProtoPure;
2008-03-27 ago nonfix >>;
2008-03-26 ago added thread data (formerly global ref in ML/ml_context.ML);
2007-09-08 ago removed thy_ord (erratic due to multi-threading);
2007-08-20 ago tuned CRITICAL sections;
2007-08-08 ago thread-safeness: when creating certified items, perform Theory.check_thy *last*;
2007-08-03 ago improved check_thy: produce a checked theory_ref (thread-safe version);
2007-07-23 ago marked some CRITICAL sections;
2007-07-05 ago the_theory/proof: error instead of exception Fail;
2007-06-13 ago merge/merge_refs: plain error instead of exception TERM;
2007-05-07 ago simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
2007-04-30 ago removed obsolete get_sg;
2007-04-05 ago added thy_ord -- order of creation;
2007-04-04 ago theory: maintain ancestors in order of creation;
2007-01-21 ago *** MESSAGE REFERS TO PREVIOUS VERSION ***
2007-01-21 ago tuned comments