src/Pure/Isar/method.ML
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-08-28 wenzelm 2014-08-28 intern xthm only once;
2014-08-27 wenzelm 2014-08-27 more explicit Method.modifier with reported position;
2014-08-22 wenzelm 2014-08-22 attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";
2014-08-22 wenzelm 2014-08-22 made SML/NJ happy;
2014-08-21 wenzelm 2014-08-21 clarified Method.section: explicit declaration with static closure;
2014-08-21 wenzelm 2014-08-21 tuned;
2014-08-21 wenzelm 2014-08-21 tuned;
2014-08-20 wenzelm 2014-08-20 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
2014-08-20 wenzelm 2014-08-20 more uniform data slot;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-08-19 wenzelm 2014-08-19 just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
2014-08-19 wenzelm 2014-08-19 tuned signature;
2014-08-19 wenzelm 2014-08-19 more compact datatypes;
2014-08-19 wenzelm 2014-08-19 tuned;
2014-08-19 wenzelm 2014-08-19 clarifed Method.evaluate: turn text into semantic method (like Basic);
2014-08-19 wenzelm 2014-08-19 simplified type Proof.method;
2014-08-14 wenzelm 2014-08-14 localized command 'method_setup' and 'attribute_setup'; clarified (non)application of morphism: argument src is already transformed, semantic body remains untransformed;
2014-08-14 wenzelm 2014-08-14 tuned;
2014-08-14 wenzelm 2014-08-14 tuned;
2014-08-14 wenzelm 2014-08-14 localized method definitions (see also f14c1248d064);
2014-08-05 wenzelm 2014-08-05 avoid duplication of warnings stemming from simp/intro declarations etc.;
2014-04-09 wenzelm 2014-04-09 proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-25 wenzelm 2014-03-25 separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-20 wenzelm 2014-03-20 more static checking of proof methods;
2014-03-18 wenzelm 2014-03-18 more antiquotations;
2014-03-18 wenzelm 2014-03-18 tuned signature;
2014-03-11 wenzelm 2014-03-11 tuned signature;
2014-03-10 wenzelm 2014-03-10 clarified Args.check_src: retain name space information for error output; tuned signature;
2014-03-10 wenzelm 2014-03-10 clarified Args.src: more abstract type, position refers to name only; prefer self-contained Args.check_src;
2014-03-10 wenzelm 2014-03-10 tuned signature -- prefer Name_Space.get with its builtin error;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
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-05 wenzelm 2014-03-05 special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
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 markup for method combinators;
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-24 wenzelm 2014-02-24 clarified Token.range_of in accordance to Symbol_Pos.range; eliminated redundant Position.set_range, which is already included in Position.range;
2014-02-24 wenzelm 2014-02-24 tuned signature;
2014-01-19 wenzelm 2014-01-19 implicit "cartouche" method (experimental, undocumented);
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-08-23 wenzelm 2013-08-23 tuned signature;
2013-08-16 wenzelm 2013-08-16 more markup via Name_Space.check; tuned signature;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-03-30 wenzelm 2013-03-30 more item markup; tuned signature;
2013-03-27 wenzelm 2013-03-27 clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;
2013-03-09 wenzelm 2013-03-09 tuned;
2012-11-30 wenzelm 2012-11-30 print formal entities with markup;
2012-10-17 wenzelm 2012-10-17 more method position information, notably finished_pos after end of previous text;
2012-10-16 wenzelm 2012-10-16 more proof method text position information;
2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-10-13 wenzelm 2012-10-13 refined Proof.the_finished_goal with more informative error; more permissive Method.all_assm_tac: do not insist in solving by assumption here to postpone failure; clarified Method.finish_text: no Thm.no_prems filtering here to postpone failure;