src/Pure/Thy/document_antiquotations.ML
2017-06-12 wenzelm 2017-06-12 more markup for HTML rendering;
2016-08-12 wenzelm 2016-08-12 clarified syntax;
2016-05-23 wenzelm 2016-05-23 embedded content may be delimited via cartouches;
2016-04-01 wenzelm 2016-04-01 tuned signature;
2016-03-05 wenzelm 2016-03-05 more PIDE markup;
2016-02-02 wenzelm 2016-02-02 proper markup for formal text;
2016-01-22 wenzelm 2016-01-22 tuned markup, e.g. relevant for Rendering.tooltip;
2016-01-12 wenzelm 2016-01-12 more explicit errors for control symbols that are left-over after Markdown parsing;
2016-01-05 wenzelm 2016-01-05 updated headers;
2015-12-09 wenzelm 2015-12-09 clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;
2015-11-25 wenzelm 2015-11-25 observe option "indent";
2015-11-19 wenzelm 2015-11-19 trim lines for @{theory_text} similarly to @{text};
2015-11-19 wenzelm 2015-11-19 tuned;
2015-11-13 wenzelm 2015-11-13 added antiquotation @{doc}, e.g. useful for demonstration purposes;
2015-11-10 wenzelm 2015-11-10 added @{command}, @{method}, @{attribute};
2015-11-10 wenzelm 2015-11-10 clarified modules;