src/Pure/codegen.ML
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
2008-09-22 haftmann 2008-09-22 some steps towards generic quickcheck framework
2008-09-18 wenzelm 2008-09-18 eval_term: CRITICAL due to eval_result; simplified oracle interface;
2008-09-17 wenzelm 2008-09-17 simplified ML_Context.eval_in -- expect immutable Proof.context value; parse_code: operate on thy, which contains the ML environment;
2008-09-16 haftmann 2008-09-16 generic value command
2008-08-28 haftmann 2008-08-28 restructured and split code serializer module
2008-08-06 berghofe 2008-08-06 Reverted last change, since it caused incompatibilities.
2008-08-04 berghofe 2008-08-04 Quoted terms in consts_code declarations are now preprocessed as well.
2008-06-30 haftmann 2008-06-30 simplified retrieval of theory names of consts and types
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-20 haftmann 2008-06-20 type constructors now with markup
2008-06-18 wenzelm 2008-06-18 OldGoals.simple_read_term;
2008-05-23 berghofe 2008-05-23 Replaced Pretty.str and Pretty.string_of by specific functions that set print_mode and margin appropriately.
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-04-17 wenzelm 2008-04-17 Pretty.mark;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-24 wenzelm 2008-03-24 ML runtime compilation: pass position, tuned signature;
2008-01-10 berghofe 2008-01-10 Test data generation and conversion to terms are now more closely intertwined, to allow displaying of functions in test data.
2007-11-11 wenzelm 2007-11-11 auto quickcheck: reduced messages;
2007-11-10 wenzelm 2007-11-10 auto_quickcheck ref: set default in ProofGeneral/preferences only (retains responsiveness of plain tty interaction); auto_quickcheck: more messages, less complicated code;
2007-11-09 haftmann 2007-11-09 explicit message for failed autoquickcheck
2007-11-08 wenzelm 2007-11-08 oops -- avoid vacous goal message; tuned messages;
2007-11-08 wenzelm 2007-11-08 tuned messages; tuned;
2007-11-06 haftmann 2007-11-06 autoquickcheck message
2007-10-12 wenzelm 2007-10-12 eval_term: moved actual evaluation out of CRITICAL section;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-08 wenzelm 2007-10-08 Codegen.is_instance: raw match, ignore sort constraints; replaced get_axiom by authentic get_axiom_i;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-01 wenzelm 2007-10-01 auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-09-24 wenzelm 2007-09-24 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
2007-09-20 berghofe 2007-09-20 - eval_term no longer computes result during compile time - generated ML code is now compiled via ML_Context.use_mltext rather than use_text; this makes sure that antiquotations are expanded - quickcheck now checks whether types to be substituted for type variables have correct sorts; this avoids spurious counterexamples - execution time for auto_quickcheck is now limited
2007-09-18 wenzelm 2007-09-18 simplified PrintMode interfaces;
2007-09-15 haftmann 2007-09-15 tuned
2007-09-10 berghofe 2007-09-10 Auto quickcheck now displays counterexample using Proof.goal_message rather than producing an error message.
2007-09-01 wenzelm 2007-09-01 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
2007-08-29 berghofe 2007-08-29 Deleted unused fillin_mixfix function.
2007-08-28 berghofe 2007-08-28 - restored old setup - new infrastructure for auto quickcheck - fixed bug in eta_expand that caused argument types to get mixed up
2007-08-16 haftmann 2007-08-16 fixed codegen setup