src/Pure/Thy/thy_output.ML
2017-06-06 wenzelm 2017-06-06 tuned signature;
2017-02-04 wenzelm 2017-02-04 more uniform use of Reconstruct.clean_proof_of;
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-10-23 wenzelm 2016-10-23 tuned signature: avoid conflict with "paragraph" as section heading;
2016-07-24 haftmann 2016-07-24 text antiquotation for locales (similar to classes)
2016-05-23 wenzelm 2016-05-23 embedded content may be delimited via cartouches;
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-03-29 wenzelm 2016-03-29 clarified reports; tuned signature;
2016-02-28 wenzelm 2016-02-28 discontinued old 'header';
2015-12-20 wenzelm 2015-12-20 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
2015-12-19 wenzelm 2015-12-19 tuned signature;
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-10 wenzelm 2015-11-10 clarified modules;
2015-11-10 wenzelm 2015-11-10 added document antiquotation @{theory_text}; tuned document;
2015-11-07 wenzelm 2015-11-07 clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
2015-11-06 wenzelm 2015-11-06 more formal treatment of control symbols;
2015-11-05 wenzelm 2015-11-05 symbolic syntax "\<comment> text";
2015-11-04 wenzelm 2015-11-04 document antiquotation @{footnote}; render \<^footnote> as pilcrow -- the rarely used \<paragraph> loses its interpretation;
2015-11-02 wenzelm 2015-11-02 clarified completion of Isabelle symbols within document source;
2015-10-21 wenzelm 2015-10-21 tuned;
2015-10-20 wenzelm 2015-10-20 another antiquotation short form: undecorated cartouche as alias for @{text}; document antiquotation @{text} ignores option "source";
2015-10-18 wenzelm 2015-10-18 clarified control antiquotations: decode control symbol to get name; document antiquotations @{emph}, @{bold}; symbol interpretation for \<^emph>; tuned;
2015-10-18 wenzelm 2015-10-18 support control symbol antiquotations;
2015-10-17 wenzelm 2015-10-17 clarified Latex.environment;
2015-10-17 wenzelm 2015-10-17 more explicit output of list items;
2015-10-17 wenzelm 2015-10-17 clarified nesting of paragraphs: indentation is taken into account more uniformly; tuned;
2015-10-16 wenzelm 2015-10-16 Markdown support in document text;
2015-10-16 wenzelm 2015-10-16 clarified Antiquote.antiq_reports; Thy_Output.output_text: support for markdown (inactive); eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;
2015-10-15 wenzelm 2015-10-15 trim_blanks after read, before eval; clarified Raw_Token: uniform output_text; tuned signature;
2015-10-15 wenzelm 2015-10-15 clarified modules;
2015-10-13 wenzelm 2015-10-13 tuned signature (cf. XML.trim_blanks);
2015-08-28 wenzelm 2015-08-28 clarified language context, e.g. relevant for symbols;
2015-04-16 wenzelm 2015-04-16 clarified document antiquotation: same check as in ML antiquotation;
2015-04-16 wenzelm 2015-04-16 explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;
2015-04-06 wenzelm 2015-04-06 support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 wenzelm 2015-04-04 more general notion of command span: command keyword not necessarily at start; support for special 'private' prefix for local_theory commands; clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;
2015-04-03 wenzelm 2015-04-03 more uniform "verbose" option to print name space;
2015-03-25 wenzelm 2015-03-25 tuned signature;
2014-12-22 wenzelm 2014-12-22 system option "pretty_margin" is superseded by "thy_output_margin";
2014-11-30 wenzelm 2014-11-30 tuned signature;
2014-11-30 wenzelm 2014-11-30 tuned signature;
2014-11-30 wenzelm 2014-11-30 tuned signature -- prefer Input.source;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-13 wenzelm 2014-11-13 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;
2014-11-12 wenzelm 2014-11-12 make SML/NJ happy;
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 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-11-06 wenzelm 2014-11-06 more explicit Keyword.keywords;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-11-01 wenzelm 2014-11-01 clarified syntax -- avoid overlap with command category;
2014-11-01 wenzelm 2014-11-01 recover via scanner; tuned signature;
2014-11-01 wenzelm 2014-11-01 command-line terminator ";" is no longer accepted;
2014-10-21 wenzelm 2014-10-21 clarified verbatim line breaks, e.g. relevant for Implementation mldecls;
2014-10-20 wenzelm 2014-10-20 official support for "tt" style variants, avoid fragile \verb in LaTeX; official document antiquotation @{verbatim};
2014-08-28 wenzelm 2014-08-28 more liberal embedded "text", which includes cartouches;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-05-24 wenzelm 2014-05-24 strip trailing white space, to avoid notorious problems of jEdit with last line;
2014-04-12 wenzelm 2014-04-12 markup for prose words within formal comments;
2014-04-06 wenzelm 2014-04-06 more source positions;