src/Pure/Thy/thy_output.ML
2014-03-25 ago added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-18 ago more antiquotations;
2014-03-18 ago tuned signature;
2014-03-12 ago simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
2014-03-11 ago tuned signature;
2014-03-10 ago some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
2014-03-10 ago clarified Args.check_src: retain name space information for error output;
2014-03-10 ago clarified Args.src: more abstract type, position refers to name only;
2014-03-10 ago tuned signature;
2014-03-09 ago tuned signature;
2014-03-06 ago more uniform check_const/read_const;
2014-03-06 ago tuned signature -- more uniform check_type_name/read_type_name;
2014-03-02 ago clarified names of antiquotations and markup;
2014-03-01 ago tuned signature;
2014-03-01 ago clarified language markup: added "delimited" property;
2014-02-28 ago tuned errors -- in accordance to ML antiquotations;
2014-02-28 ago more explicit method reports;
2014-02-26 ago method language markup, e.g. relevant to prevent outer keyword completion;
2014-02-25 ago proper context for global data;
2014-02-25 ago more markup;
2014-02-19 ago prefer guarded Context_Position.report where feasible;
2014-02-18 ago more markup;
2014-02-18 ago generic markup for embedded languages;
2014-02-17 ago more markup;
2014-01-22 ago tuned signature;
2013-12-09 ago added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
2013-08-23 ago added Theory.setup convenience;
2013-08-23 ago discontinued unused antiquotation blocks;
2013-08-16 ago more markup via Name_Space.check;
2013-05-16 ago Thy_Output.modes as proper option;
2013-05-16 ago some system options as context-sensitive config options;
2013-05-13 ago retain goal display options when printing error messages, to avoid breakdown for huge goals;
2013-04-05 ago tuned signature -- agree with markup terminology;
2013-04-05 ago unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
2013-03-27 ago more liberal handling of skipped proofs;
2013-02-24 ago tuned;
2012-12-18 ago discontinued legacy antiquotations and styles
2012-11-30 ago print formal entities with markup;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-13 ago some attempts to unify/simplify pretty_goal;
2012-09-12 ago avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);
2012-09-10 ago formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
2012-08-29 ago renamed Position.str_of to Position.here;
2012-08-26 ago theory def/ref position reports, which enable hyperlinks etc.;
2012-08-24 ago check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-16 ago define keywords early when processing the theory header, before running the body commands;
2012-03-16 ago clarified Keyword.is_keyword: union of minor and major;
2012-03-15 ago declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 ago declare minor keywords via theory header;
2012-03-14 ago tuned;
2012-03-14 ago source positions for locale and class expressions;
2012-03-04 ago clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
2012-01-25 ago document antiquotations for ML infix operators;
2012-01-12 ago tuned;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-07-23 ago defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-06-27 ago document antiquotations are managed as theory data, with proper name space and entity markup;
2011-05-03 ago more conventional naming scheme: names_long, names_short, names_unique;
2011-05-02 ago added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;