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;
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;
2011-04-30 ago allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
2011-04-18 ago pretty_abbrev: read abbreviation more directly;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago prefer local name spaces;
2011-04-16 ago Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 ago explicit structure Syntax_Trans;
2010-12-02 ago configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-11-29 ago added document antiquotation @{file};
2010-11-28 ago Parse.liberal_name for document antiquotations and attributes;
2010-09-24 ago clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
2010-09-17 ago tuned signature of (Context_) variants;
2010-09-13 ago type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input
2010-09-13 ago merged
2010-09-13 ago 'class' and 'type' are now antiquoations by default
2010-09-12 ago eliminated aliases of Type.constraint;
2010-09-05 ago turned show_sorts/show_types into proper configuration options;
2010-09-04 ago recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);
2010-09-03 ago turned eta_contract into proper configuration option;
2010-09-03 ago turned show_structs into proper configuration option;
2010-09-03 ago pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-09-02 ago turned show_question_marks into proper configuration option;
2010-08-27 ago eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;
2010-08-27 ago proper context for various Thy_Output options, via official configuration options in ML and Isar;
2010-08-27 ago Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-30 ago replaced ML_Lex.read_antiq by more concise, which includes full read/report with explicit position information;
2010-05-27 ago renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-17 ago renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-05-08 ago unified/simplified Pretty.margin_default;
2010-04-28 ago term_typ: print styled term
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-04-16 ago proper checking of ML functors (in Poly/ML 5.2 or later);
2010-02-27 ago clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-02 ago modernized structure Proof_Syntax;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;