src/Pure/Isar/attrib.ML
17 months ago ago disallow pending hyps;
21 months ago ago support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
22 months ago ago clarified signature;
22 months ago ago more operations;
2017-12-06 ago prefer control symbol antiquotations;
2016-12-13 ago more symbols;
2016-06-23 ago tuned signature;
2016-06-21 ago tuned;
2016-06-09 ago tuned signature;
2016-06-09 ago tuned;
2016-05-12 ago common entity definitions within a global or local theory context;
2016-04-28 ago unfold is subject to unfold_abs_def (still inactive);
2016-04-18 ago prefer internal attribute source;
2016-04-07 ago Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
2016-04-05 ago clarified modules -- simplified bootstrap;
2016-04-01 ago removed redundant Position.set_range -- already done in Position.range;
2016-03-02 ago support for ML_exception_debugger;
2015-12-15 ago unused;
2015-12-09 ago tuned;
2015-12-09 ago unused;
2015-12-09 ago clarified type Token.src: plain token list, with usual implicit value assignment;
2015-10-30 ago tuned signature -- clarified modules;
2015-10-18 ago tuned signature;
2015-09-25 ago moved remaining display.ML to more_thm.ML;
2015-07-17 ago proper attribute;
2015-05-03 ago tuned output;
2015-05-03 ago tuned output -- avoid empty quites and extra breaks;
2015-04-03 ago more uniform "verbose" option to print name space;
2014-11-30 ago more abstract type Input.source;
2014-11-12 ago more careful ML source positions, for improved PIDE markup;
2014-11-11 ago more careful ML source positions, for improved PIDE markup;
2014-11-11 ago more position information, e.g. relevant for errors in generated ML source;
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-11-05 ago explicit type Keyword.keywords;
2014-11-01 ago tuned signature (see ab2483fad861);
2014-08-27 ago tuned signature -- prefer quasi-abstract Symbol_Pos.source;
2014-08-25 ago tuned signature;
2014-08-21 ago tuned signature -- define some elementary operations earlier;
2014-08-21 ago tuned;
2014-08-19 ago tuned signature -- moved type src to Token, without aliases;
2014-08-14 ago more informative Token.Fact: retain name of dynamic fact (without selection);
2014-08-14 ago localized command 'method_setup' and 'attribute_setup';
2014-08-14 ago tuned;
2014-08-14 ago tuned;
2014-08-14 ago tuned signature;
2014-08-13 ago localized attribute definitions;
2014-08-05 ago refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
2014-04-06 ago more source positions;
2014-04-06 ago more source positions;
2014-03-31 ago some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-27 ago clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-25 ago proper configuration option "ML_print_depth";
2014-03-25 ago clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
2014-03-25 ago separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-24 ago discontinued Toplevel.debug in favour of system option "exception_trace";
2014-03-14 ago just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
2014-03-11 ago tuned signature;
2014-03-10 ago more markup;
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;