doc-src/antiquote_setup.ML
2012-02-18 haftmann 2012-02-18 avoid redefinition of @{theory} antiquotation
2012-02-18 haftmann 2012-02-18 more precise semantics of "theory" antiquotation
2012-01-25 wenzelm 2012-01-25 document antiquotations for ML infix operators;
2011-11-29 bulwahn 2011-11-29 adjusting antiquote_setup (cf. d83797ef0d2d)
2011-06-27 wenzelm 2011-06-27 document antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27 wenzelm 2011-06-27 proper checking of @{ML_antiquotation};
2011-05-03 wenzelm 2011-05-03 use existing \<hyphen>;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2010-11-29 wenzelm 2010-11-29 added document antiquotation @{file};
2010-10-19 wenzelm 2010-10-19 more robust treatment of "op IDENT";
2010-10-19 wenzelm 2010-10-19 more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
2010-10-16 wenzelm 2010-10-16 more robust treatment of symbolic indentifiers (which may contain colons);
2010-10-08 wenzelm 2010-10-08 more on ML antiquotations; tuned;
2010-08-27 wenzelm 2010-08-27 proper context for various Thy_Output options, via official configuration options in ML and Isar;
2010-07-27 wenzelm 2010-07-27 updated manual concerning theory loader;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
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-18 wenzelm 2010-05-18 prefer structure Keyword and Parse;
2010-04-16 wenzelm 2010-04-16 proper checking of ML functors (in Poly/ML 5.2 or later); eliminated pathetic comments;
2009-06-10 wenzelm 2009-06-10 eliminated escaped symbols;
2009-05-30 wenzelm 2009-05-30 tuned;
2009-03-09 wenzelm 2009-03-09 fornal markup for antiquotation options;
2009-03-09 wenzelm 2009-03-09 moved @{ML_functor} and @{ML_text} to Pure; adapted to simplified ThyOutput.antiquotation interface; misc tuning;
2009-03-09 wenzelm 2009-03-09 adapted ThyOutput.antiquotation;
2009-03-08 wenzelm 2009-03-08 use simplified ThyOutput.antiquotation; eliminated obscure structure alias;
2009-03-08 wenzelm 2009-03-08 adapted to structure Long_Name;
2009-03-08 wenzelm 2009-03-08 index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-26 wenzelm 2009-02-26 uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities; more robust handling of "|" within index;
2009-02-14 wenzelm 2009-02-14 clean_string/clean_name: proper treatment of \<dash>;
2009-02-11 wenzelm 2009-02-11 added "inference" entity;
2008-11-13 wenzelm 2008-11-13 ignore ThyOutput.source flag;
2008-10-21 wenzelm 2008-10-21 ThyOutput: export some auxiliary operations;
2008-09-29 haftmann 2008-09-29 added theory antiquotation
2008-09-17 wenzelm 2008-09-17 simplified ML_Context.eval_in -- expect immutable Proof.context value;
2008-09-16 wenzelm 2008-09-16 check setting and tool; added file;
2008-09-15 wenzelm 2008-09-15 tuned comment;
2008-09-15 wenzelm 2008-09-15 added formal markup for setting, executable, tool;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-05-15 wenzelm 2008-05-15 tuned clean_name (underscore);
2008-05-15 wenzelm 2008-05-15 clean_name: replace "_" by "-";
2008-05-15 wenzelm 2008-05-15 clean_string: cover <; added clean_name; output_entity: hyperlink;
2008-05-14 wenzelm 2008-05-14 proper checking of various Isar elements;
2008-05-08 wenzelm 2008-05-08 clean_string: map "_" to "\\_" (best used with underscore.sty);
2008-05-07 wenzelm 2008-05-07 output_entity: ignore ThyOutput.source option;
2008-05-06 wenzelm 2008-05-06 element: isakeyword markup;
2008-05-02 wenzelm 2008-05-02 output_entity: added \mbox{} to prevent hyphenation;
2008-05-02 wenzelm 2008-05-02 clean_string: handle { };
2008-04-28 wenzelm 2008-04-28 proper command/keyword markup;
2008-04-26 wenzelm 2008-04-26 added setup for Isar entities; tuned;
2008-04-23 wenzelm 2008-04-23 misc cleanup;
2008-04-17 wenzelm 2008-04-17 pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
2008-03-28 haftmann 2008-03-28 some styling
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-24 wenzelm 2008-03-24 ML runtime compilation: pass position, tuned signature;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-09-15 haftmann 2007-09-15 fixed title