src/Pure/Isar/isar_syn.ML
2014-04-19 wenzelm 2014-04-19 added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
2014-04-08 wenzelm 2014-04-08 more uniform ML/document antiquotations;
2014-03-31 wenzelm 2014-03-31 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
2014-03-27 wenzelm 2014-03-27 redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); more explicit ML_Compiler.flags;
2014-03-25 wenzelm 2014-03-25 added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-15 wenzelm 2014-03-15 more explicit treatment of verbose mode, which includes concealed entries;
2014-03-15 wenzelm 2014-03-15 clarified print_local_facts;
2014-03-12 wenzelm 2014-03-12 simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; added command 'print_ML_antiquotations';
2014-03-12 wenzelm 2014-03-12 more explicit markup and explanation of the improper status of 'back', following the AFP style-guide;
2014-03-09 wenzelm 2014-03-09 more formal read_root;
2014-03-09 wenzelm 2014-03-09 simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
2014-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-28 wenzelm 2014-02-28 more explicit method reports; avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);
2014-02-26 wenzelm 2014-02-26 method language markup, e.g. relevant to prevent outer keyword completion;
2014-02-25 wenzelm 2014-02-25 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion; removed obsolete Method.Source_i; proper context for global data; tuned messages;
2014-02-10 wenzelm 2014-02-10 discontinued axiomatic 'classes', 'classrel', 'arities';
2014-01-25 wenzelm 2014-01-25 prefer self-contained user-space tool;
2013-09-30 wenzelm 2013-09-30 tuned;
2013-09-04 wenzelm 2013-09-04 some explicit indication of Proof General legacy;
2013-09-03 wenzelm 2013-09-03 cases: more position information and PIDE markup;
2013-09-03 wenzelm 2013-09-03 more liberal 'case' syntax: allow parentheses without arguments;
2013-07-07 wenzelm 2013-07-07 discontinued command 'print_drafts';
2013-07-07 wenzelm 2013-07-07 tuned comments;
2013-06-24 wenzelm 2013-06-24 back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;
2013-06-23 wenzelm 2013-06-23 proper diagnostic command 'print_state';
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-05-17 wenzelm 2013-05-17 renamed 'print_configs' to 'print_options';
2013-05-14 wenzelm 2013-05-14 more antiquotations;
2013-05-13 wenzelm 2013-05-13 option "goals_limit", with more uniform description;
2013-04-23 haftmann 2013-04-23 target-sensitive user-level commands interpretation and sublocale
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-04-09 wenzelm 2013-04-09 discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
2013-04-09 wenzelm 2013-04-09 just one syntax category "mixfix" -- check structure annotation semantically;
2013-04-05 wenzelm 2013-04-05 tuned signature -- agree with markup terminology;
2013-03-30 wenzelm 2013-03-30 added 'print_defn_rules' command; tuned;
2013-02-28 wenzelm 2013-02-28 discontinued obsolete 'axioms' command;
2013-02-27 wenzelm 2013-02-27 discontinued redundant 'use' command;
2013-01-05 wenzelm 2013-01-05 tuned -- less indirection;
2012-11-26 wenzelm 2012-11-26 tuned command descriptions;
2012-11-26 wenzelm 2012-11-26 refined outer syntax 'help' command;
2012-10-16 wenzelm 2012-10-16 more informative errors for 'also' and 'finally';
2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-10-16 wenzelm 2012-10-16 more informative errors for 'proof' and 'apply' steps; more Seq.result operations;
2012-09-26 wenzelm 2012-09-26 tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that; added command 'locale_deps'; graphview prints plain text only -- removed dependency on old Cobra HTML_Panel;
2012-08-29 wenzelm 2012-08-29 command 'use' is legacy;
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
2012-08-22 wenzelm 2012-08-22 clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-14 wenzelm 2012-08-14 support for 'typ' with explicit sort constraint;
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position;
2012-08-02 wenzelm 2012-08-02 more antiquotations;
2012-08-02 wenzelm 2012-08-02 more antiquotations;
2012-08-02 wenzelm 2012-08-02 more antiquotations;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure outer syntax;
2012-04-10 wenzelm 2012-04-10 static relevance of proof via syntax keywords;
2012-04-01 wenzelm 2012-04-01 more general context command with auxiliary fixes/assumes etc.;
2012-03-21 wenzelm 2012-03-21 more explicit Toplevel.open_target/close_target; replaced 'context_includes' by 'context' 'includes'; tuned command descriptions;