src/Pure/Isar/method.ML
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
Tue, 19 Aug 2014 16:46:07 +0200 wenzelm just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
Tue, 19 Aug 2014 16:09:11 +0200 wenzelm tuned signature;
Tue, 19 Aug 2014 15:55:06 +0200 wenzelm more compact datatypes;
Tue, 19 Aug 2014 15:10:37 +0200 wenzelm tuned;
Tue, 19 Aug 2014 14:51:25 +0200 wenzelm clarifed Method.evaluate: turn text into semantic method (like Basic);
Tue, 19 Aug 2014 12:05:11 +0200 wenzelm simplified type Proof.method;
Thu, 14 Aug 2014 14:28:11 +0200 wenzelm localized command 'method_setup' and 'attribute_setup';
Thu, 14 Aug 2014 12:33:21 +0200 wenzelm tuned;
Thu, 14 Aug 2014 12:13:24 +0200 wenzelm tuned;
Thu, 14 Aug 2014 11:51:17 +0200 wenzelm localized method definitions (see also f14c1248d064);
Tue, 05 Aug 2014 15:07:11 +0200 wenzelm avoid duplication of warnings stemming from simp/intro declarations etc.;
Wed, 09 Apr 2014 20:58:32 +0200 wenzelm proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Tue, 25 Mar 2014 16:11:00 +0100 wenzelm separate tokenization and language context for SML: no symbols, no antiquotes;
Thu, 20 Mar 2014 22:00:13 +0100 wenzelm more static checking of proof methods;
Tue, 18 Mar 2014 15:29:58 +0100 wenzelm more antiquotations;
Tue, 18 Mar 2014 11:27:09 +0100 wenzelm tuned signature;
Tue, 11 Mar 2014 14:28:39 +0100 wenzelm tuned signature;
Mon, 10 Mar 2014 18:06:23 +0100 wenzelm clarified Args.check_src: retain name space information for error output;
Mon, 10 Mar 2014 16:30:07 +0100 wenzelm clarified Args.src: more abstract type, position refers to name only;
Mon, 10 Mar 2014 15:04:01 +0100 wenzelm tuned signature -- prefer Name_Space.get with its builtin error;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Sat, 08 Mar 2014 21:08:10 +0100 wenzelm modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
Wed, 05 Mar 2014 15:25:52 +0100 wenzelm special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Fri, 28 Feb 2014 10:40:04 +0100 wenzelm more explicit method reports;
Wed, 26 Feb 2014 11:58:35 +0100 wenzelm markup for method combinators;
Wed, 26 Feb 2014 10:40:13 +0100 wenzelm method language markup, e.g. relevant to prevent outer keyword completion;
Tue, 25 Feb 2014 14:34:18 +0100 wenzelm modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
less more (0) -100 -50 -30 tip