4 months ago ago clarified signature;
11 months ago ago tuned signature;
11 months ago ago clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
13 months ago ago markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
14 months ago ago adjust position according to offset of command/exec id;
17 months ago ago clarified signature;
18 months ago ago clarified signature;
18 months ago ago tuned message;
18 months ago ago clarified operations;
18 months ago ago tuned signature: removed unused operations;
18 months ago ago clarified signature;
18 months ago ago clarified operations;
18 months ago ago discontinued old form of marginal comments;
18 months ago ago clarified markup;
18 months ago ago more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
2017-06-12 ago more markup for HTML rendering;
2017-06-12 ago tuned signature;
2017-06-08 ago more HTML rendering as in Isabelle/jEdit;
2017-03-10 ago avoid extra decorations for regular command keywords;
2016-12-28 ago more uniform treatment of "bad" like other messages (with serial number);
2016-10-27 ago more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
2016-09-22 ago discontinued raw symbols;
2016-08-09 ago print name in parsable form;
2016-04-18 ago prefer internal attribute source;
2016-04-13 ago eliminated "xname" and variants;
2016-04-01 ago tuned signature;
2016-04-01 ago tuned;
2016-04-01 ago tuned signature;
2016-03-31 ago clarified modules;
2016-01-07 ago prefer non-ASCII output;
2015-12-10 ago make SML/NJ happy;
2015-12-09 ago tuned;
2015-12-09 ago tuned signature;
2015-12-09 ago tuned;
2015-12-09 ago clarified type Token.src: plain token list, with usual implicit value assignment;
2015-11-10 ago added document antiquotation @{theory_text};
2015-10-18 ago tuned signature;
2015-10-18 ago support control symbol antiquotations;
2015-09-25 ago moved remaining display.ML to more_thm.ML;
2015-09-02 ago trim context more thoroughly;
2015-05-01 ago modifier markup for all parsed tokens;
2015-04-09 ago clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-06 ago support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 ago more general notion of command span: command keyword not necessarily at start;
2015-04-02 ago tuned signature;
2015-04-02 ago operation on embedded sources for Eisbach;
2015-04-02 ago tuned -- emphasize semantics of already checked src;
2015-03-25 ago tuned signature;
2015-03-24 ago clarified input source;
2015-03-10 ago clarified Token.check_src: intern at most once;
2015-03-07 ago added declare_maxidx operations for Eisbach;
2014-12-10 ago more explicit markup for improper commands;
2014-12-10 ago tuned;
2014-12-09 ago imitate command markup and rendering of Isabelle/jEdit in HTML output;
2014-12-08 ago expand ML cartouches to Input.source;
2014-12-03 ago clarified define_command: send tokens more directly, without requiring keywords in ML;
2014-12-03 ago tuned signature;
2014-12-03 ago clarified token kind;
2014-11-30 ago more abstract type Input.source;
2014-11-11 ago more position information, e.g. relevant for errors in generated ML source;