src/Pure/Thy/thy_output.ML
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;
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;