src/Pure/Isar/isar_syn.ML
2014-03-25 ago added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-21 ago tuned signature;
2014-03-21 ago tuned signature;
2014-03-15 ago more explicit treatment of verbose mode, which includes concealed entries;
2014-03-15 ago clarified print_local_facts;
2014-03-12 ago simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
2014-03-12 ago more explicit markup and explanation of the improper status of 'back', following the AFP style-guide;
2014-03-09 ago more formal read_root;
2014-03-09 ago simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
2014-03-08 ago modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
2014-03-01 ago clarified language markup: added "delimited" property;
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 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
2014-02-10 ago discontinued axiomatic 'classes', 'classrel', 'arities';
2014-01-25 ago prefer self-contained user-space tool;
2013-09-30 ago tuned;
2013-09-04 ago some explicit indication of Proof General legacy;
2013-09-03 ago cases: more position information and PIDE markup;
2013-09-03 ago more liberal 'case' syntax: allow parentheses without arguments;
2013-07-07 ago discontinued command 'print_drafts';
2013-07-07 ago tuned comments;
2013-06-24 ago back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;
2013-06-23 ago proper diagnostic command 'print_state';
2013-05-25 ago syntax translations always depend on context;
2013-05-17 ago renamed 'print_configs' to 'print_options';
2013-05-14 ago more antiquotations;
2013-05-13 ago option "goals_limit", with more uniform description;
2013-04-23 ago target-sensitive user-level commands interpretation and sublocale
2013-04-18 ago simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 ago more standard module name Axclass (according to file name);
2013-04-09 ago discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2013-04-09 ago just one syntax category "mixfix" -- check structure annotation semantically;
2013-04-05 ago tuned signature -- agree with markup terminology;
2013-03-30 ago added 'print_defn_rules' command;
2013-02-28 ago discontinued obsolete 'axioms' command;
2013-02-27 ago discontinued redundant 'use' command;
2013-01-05 ago tuned -- less indirection;
2012-11-26 ago tuned command descriptions;
2012-11-26 ago refined outer syntax 'help' command;
2012-10-16 ago more informative errors for 'also' and 'finally';
2012-10-16 ago clarified defer/prefer: more specific errors;
2012-10-16 ago more informative errors for 'proof' and 'apply' steps;
2012-09-26 ago tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
2012-08-29 ago command 'use' is legacy;
2012-08-26 ago theory def/ref position reports, which enable hyperlinks etc.;
2012-08-22 ago clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-14 ago support for 'typ' with explicit sort constraint;
2012-08-02 ago more official command specifications, including source position;
2012-08-02 ago more antiquotations;
2012-08-02 ago more antiquotations;
2012-08-02 ago more antiquotations;
2012-08-01 ago more standard bootstrapping of Pure outer syntax;
2012-04-10 ago static relevance of proof via syntax keywords;
2012-04-01 ago more general context command with auxiliary fixes/assumes etc.;
2012-03-21 ago more explicit Toplevel.open_target/close_target;
2012-03-21 ago optional 'includes' element for long theorem statements;
2012-03-21 ago basic support for nested contexts including bundles;
2012-03-20 ago basic support for bundled declarations;
2012-03-17 ago more precise syntax;