src/Pure/ML/ml_antiquote.ML
2014-03-12 wenzelm 2014-03-12 added ML antiquotation @{here};
2014-03-12 wenzelm 2014-03-12 simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; added command 'print_ML_antiquotations';
2014-03-09 wenzelm 2014-03-09 tuned signature;
2014-03-06 wenzelm 2014-03-06 eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
2014-03-06 wenzelm 2014-03-06 more uniform check_const/read_const;
2014-03-06 wenzelm 2014-03-06 tuned signature -- more uniform check_type_name/read_type_name; proper reports for read_type_name (lost in 710bc66f432c);
2014-02-19 wenzelm 2014-02-19 prefer guarded Context_Position.report where feasible;
2014-01-22 wenzelm 2014-01-22 tuned signature;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-08-23 wenzelm 2013-08-23 more robust ML_Antiquote.variant via Name.desymbolize (which also allows symbolic names, for example);
2013-08-23 wenzelm 2013-08-23 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context; subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass);
2013-08-23 wenzelm 2013-08-23 removed unused ML antiquotations @{let}, @{note};
2013-05-14 wenzelm 2013-05-14 more antiquotations;
2013-05-12 wenzelm 2013-05-12 tuned signature;
2013-05-12 wenzelm 2013-05-12 more systematic access to options default;
2013-04-10 wenzelm 2013-04-10 added ML antiquotation @{theory_context};
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
2012-08-20 wenzelm 2012-08-20 added keyword kind "thy_load" (with optional list of file extensions);
2012-08-12 wenzelm 2012-08-12 more static antiquotations;
2012-08-11 wenzelm 2012-08-11 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
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;