src/Pure/ML/ml_antiquotations.ML
2016-03-17 wenzelm 2016-03-17 @{make_string} is available during Pure bootstrap;
2016-01-24 wenzelm 2016-01-24 tuned;
2016-01-06 wenzelm 2016-01-06 added ML antiquotation @{method};
2015-11-07 wenzelm 2015-11-07 less confusing markup;
2015-11-07 wenzelm 2015-11-07 added @{undefined} with somewhat undefined symbol;
2015-11-07 wenzelm 2015-11-07 ML cartouches via control antiquotation;
2015-09-10 wenzelm 2015-09-10 removed obsolete undocumented feature;
2015-04-16 wenzelm 2015-04-16 formal Theory.check, with markup and completion;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-04-06 wenzelm 2015-04-06 more position information and PIDE markup for command keywords;
2015-03-31 wenzelm 2015-03-31 tuned message;
2015-03-25 wenzelm 2015-03-25 semantic completion for @{system_option};
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-01 wenzelm 2015-03-01 added Proof_Context.cterm_of/ctyp_of convenience;
2014-12-10 wenzelm 2014-12-10 more careful handling of auxiliary environment structure -- allow nested ML evaluation;
2014-12-08 wenzelm 2014-12-08 expand ML cartouches to Input.source; tuned signature;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-26 wenzelm 2014-11-26 added ML antiquotation @{apply n} or @{apply n(k)};
2014-11-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-11-07 wenzelm 2014-11-07 tuned;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-10-08 wenzelm 2014-10-08 tuned;
2014-08-27 wenzelm 2014-08-27 added ML antiquotation @{source} for Symbol_Pos.source;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-04-08 wenzelm 2014-04-08 more uniform ML/document antiquotations;
2014-04-08 wenzelm 2014-04-08 more positions and markup;
2014-04-04 wenzelm 2014-04-04 tuned white space;
2014-04-04 wenzelm 2014-04-04 added ML antiquotation @{print};
2014-03-22 wenzelm 2014-03-22 tuned message;
2014-03-18 wenzelm 2014-03-18 clarified modules; more antiquotations for antiquotations;