src/Pure/codegen.ML
2011-08-08 wenzelm 2011-08-08 slightly more uniform messages;
2011-07-25 bulwahn 2011-07-25 added legacy warning to old code generation evaluation
2011-07-25 bulwahn 2011-07-25 added legacy warning to old code generation commands
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-20 wenzelm 2011-04-20 eliminated global references / critical sections via context data; misc tuning and modernization;
2011-04-20 wenzelm 2011-04-20 explicit context for Codegen.eval_term etc.;
2011-04-20 wenzelm 2011-04-20 added Theory.nodes_of convenience;
2011-04-19 wenzelm 2011-04-19 eliminated Codegen.mode in favour of explicit argument;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-27 wenzelm 2011-01-27 CRITICAL markup for critical poking with unsynchronized references;
2010-12-17 wenzelm 2010-12-17 clarified exports of structure Simplifier;
2010-12-03 bulwahn 2010-12-03 adapting SML_Quickcheck to recent changes
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-03 wenzelm 2010-11-03 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-09-09 bulwahn 2010-09-09 removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
2010-08-11 wenzelm 2010-08-11 use Pretty.enum convenience;
2010-07-23 wenzelm 2010-07-23 observe standard conventions for doc-strings;
2010-05-30 wenzelm 2010-05-30 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-15 wenzelm 2010-05-15 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-05-08 wenzelm 2010-05-08 unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-25 bulwahn 2010-02-25 added basic reporting of test cases to quickcheck
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 critical comments;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 wenzelm 2009-10-25 maintain theory name via name space, not tags; AxClass.thynames_of_arity: explicit theory name, not tags;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-19 berghofe 2009-10-19 Removed dead code in function mk_deftab.
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-24 wenzelm 2009-07-24 eliminated OldGoals.read_term;
2009-07-20 haftmann 2009-07-20 deftab: only process theorems on demand
2009-07-14 haftmann 2009-07-14 more accessors to unfold simpset
2009-05-14 haftmann 2009-05-14 merged
2009-05-14 haftmann 2009-05-14 quickcheck size starts with 0
2009-05-13 berghofe 2009-05-13 Cleaned up code of function test_term.
2009-05-12 haftmann 2009-05-12 transferred code generator preprocessor into separate module
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 Thm.add_oracle interface: replaced old bstring by binding;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_vars, Term.add_frees etc.; moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-15 haftmann 2008-12-15 moved value.ML to src/Tools
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-19 berghofe 2008-10-19 - removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML) - improved code unfold preprocessor: now uses one single simpset containing all unfolding rules - got rid of some legacy functions
2008-10-09 haftmann 2008-10-09 established canonical argument order in SML code generators
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-22 haftmann 2008-09-22 generic quickcheck framework