src/Pure/ML/ml_antiquote.ML
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position;
2012-04-27 wenzelm 2012-04-27 clarified signature;
2012-03-17 wenzelm 2012-03-17 tuned message;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 added ML antiquotation @{keyword};
2011-07-13 wenzelm 2011-07-13 sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML); minor tuning;
2011-06-27 wenzelm 2011-06-27 ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-04-23 wenzelm 2011-04-23 clarified Type.the_decl;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 more accurate markup for syntax consts, notably binders which point back to the original logical entity; tuned;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-01-09 wenzelm 2011-01-09 reverted 08240feb69c7 -- breaks positions of reports;
2010-12-21 wenzelm 2010-12-21 more robust ML antiquotations -- allow original tokens without adjacent whitespace;
2010-10-28 wenzelm 2010-10-28 discontinued obsolete ML antiquotation @{theory_ref};
2010-10-25 wenzelm 2010-10-25 added ML antiquotation @{assert};
2010-07-21 wenzelm 2010-07-21 ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state; recovered @{theory_ref NAME} (cf. 1f09a22a1027);
2010-06-03 wenzelm 2010-06-03 allow qualified names;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-04-16 wenzelm 2010-04-16 added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
2010-03-09 wenzelm 2010-03-09 ProofContext.read_class/read_type_name_proper;
2010-03-03 wenzelm 2010-03-03 authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} (only logical consts) vs. @{const_abbrev}; tuned;
2010-02-27 wenzelm 2010-02-27 ML antiquotations for type classes;
2010-02-25 wenzelm 2010-02-25 more orthogonal antiquotations for type constructors;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-21 wenzelm 2010-02-21 authentic syntax for *all* term constants;
2010-02-16 wenzelm 2010-02-16 misc tuning and simplification;
2010-02-11 wenzelm 2010-02-11 added ML antiquotation @{syntax_const};
2010-02-07 wenzelm 2010-02-07 simplified interface for ML antiquotations, struct_name is always "Isabelle";
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-25 wenzelm 2009-03-25 @{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;
2009-03-15 wenzelm 2009-03-15 ML_Syntax.make_binding;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
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 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-03 wenzelm 2009-03-03 added @{binding} ML antiquotations;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-08-15 wenzelm 2008-08-15 Args.name_source(_position) for proper position information;
2008-08-14 wenzelm 2008-08-14 ML_Context.add_antiq: pass position;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-06-28 wenzelm 2008-06-28 moved theorem values to ml_thms.ML;
2008-06-28 wenzelm 2008-06-28 added macro interface; added @{let}, @{note};
2008-06-26 wenzelm 2008-06-26 Args.context;
2008-06-25 wenzelm 2008-06-25 re-use official outer keywords;
2008-06-24 wenzelm 2008-06-24 Common ML antiquotations.