src/Pure/Thy/thy_output.ML
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;
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-27 wenzelm 2014-03-27 redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); more explicit ML_Compiler.flags;
2014-03-25 wenzelm 2014-03-25 separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-25 wenzelm 2014-03-25 added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-18 wenzelm 2014-03-18 more antiquotations;
2014-03-18 wenzelm 2014-03-18 tuned signature;
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-11 wenzelm 2014-03-11 tuned signature;
2014-03-10 wenzelm 2014-03-10 some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
2014-03-10 wenzelm 2014-03-10 clarified Args.check_src: retain name space information for error output; tuned signature;
2014-03-10 wenzelm 2014-03-10 clarified Args.src: more abstract type, position refers to name only; prefer self-contained Args.check_src;
2014-03-10 wenzelm 2014-03-10 tuned signature;
2014-03-09 wenzelm 2014-03-09 tuned signature;
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-03-02 wenzelm 2014-03-02 clarified names of antiquotations and markup; more documentation;
2014-03-01 wenzelm 2014-03-01 tuned signature;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-28 wenzelm 2014-02-28 tuned errors -- in accordance to ML antiquotations;
2014-02-28 wenzelm 2014-02-28 more explicit method reports; avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);
2014-02-26 wenzelm 2014-02-26 method language markup, e.g. relevant to prevent outer keyword completion;
2014-02-25 wenzelm 2014-02-25 proper context for global data;
2014-02-25 wenzelm 2014-02-25 more markup;
2014-02-19 wenzelm 2014-02-19 prefer guarded Context_Position.report where feasible;
2014-02-18 wenzelm 2014-02-18 more markup;
2014-02-18 wenzelm 2014-02-18 generic markup for embedded languages;
2014-02-17 wenzelm 2014-02-17 more markup;
2014-01-22 wenzelm 2014-01-22 tuned signature;
2013-12-09 wenzelm 2013-12-09 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-08-23 wenzelm 2013-08-23 discontinued unused antiquotation blocks;
2013-08-16 wenzelm 2013-08-16 more markup via Name_Space.check; tuned signature;
2013-05-16 wenzelm 2013-05-16 Thy_Output.modes as proper option;
2013-05-16 wenzelm 2013-05-16 some system options as context-sensitive config options;
2013-05-13 wenzelm 2013-05-13 retain goal display options when printing error messages, to avoid breakdown for huge goals;
2013-04-05 wenzelm 2013-04-05 tuned signature -- agree with markup terminology;
2013-04-05 wenzelm 2013-04-05 unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
2013-03-27 wenzelm 2013-03-27 more liberal handling of skipped proofs;
2013-02-24 wenzelm 2013-02-24 tuned;