| Wed, 27 Aug 2014 14:54:32 +0200 |
wenzelm |
more explicit Method.modifier with reported position;
|
file |
diff |
annotate
|
| Fri, 22 Aug 2014 15:55:24 +0200 |
wenzelm |
attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";
|
file |
diff |
annotate
|
| Fri, 22 Aug 2014 11:28:51 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 23:54:27 +0200 |
wenzelm |
clarified Method.section: explicit declaration with static closure;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 13:31:31 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 09:48:59 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 20 Aug 2014 17:30:43 +0200 |
wenzelm |
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
|
file |
diff |
annotate
|
| Wed, 20 Aug 2014 16:06:10 +0200 |
wenzelm |
more uniform data slot;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 16:09:11 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 15:55:06 +0200 |
wenzelm |
more compact datatypes;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 15:10:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 14:51:25 +0200 |
wenzelm |
clarifed Method.evaluate: turn text into semantic method (like Basic);
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 12:05:11 +0200 |
wenzelm |
simplified type Proof.method;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 14:28:11 +0200 |
wenzelm |
localized command 'method_setup' and 'attribute_setup';
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 12:33:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 12:13:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 11:51:17 +0200 |
wenzelm |
localized method definitions (see also f14c1248d064);
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 15:07:11 +0200 |
wenzelm |
avoid duplication of warnings stemming from simp/intro declarations etc.;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 16:11:00 +0100 |
wenzelm |
separate tokenization and language context for SML: no symbols, no antiquotes;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2014 22:00:13 +0100 |
wenzelm |
more static checking of proof methods;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 15:29:58 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 11:27:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 14:28:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 18:06:23 +0100 |
wenzelm |
clarified Args.check_src: retain name space information for error output;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 16:30:07 +0100 |
wenzelm |
clarified Args.src: more abstract type, position refers to name only;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:04:01 +0100 |
wenzelm |
tuned signature -- prefer Name_Space.get with its builtin error;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:08:10 +0100 |
wenzelm |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 15:25:52 +0100 |
wenzelm |
special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 10:40:04 +0100 |
wenzelm |
more explicit method reports;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:58:35 +0100 |
wenzelm |
markup for method combinators;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:40:13 +0100 |
wenzelm |
method language markup, e.g. relevant to prevent outer keyword completion;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 10:48:34 +0100 |
wenzelm |
clarified Token.range_of in accordance to Symbol_Pos.range;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 10:17:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 19 Jan 2014 21:33:45 +0100 |
wenzelm |
implicit "cartouche" method (experimental, undocumented);
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 17:01:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 22:39:31 +0200 |
wenzelm |
more markup via Name_Space.check;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:41:45 +0200 |
wenzelm |
proper option quick_and_dirty;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:50:30 +0100 |
wenzelm |
clarified Skip_Proof.cheat_tac: more standard tactic;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2013 13:01:24 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2012 13:20:08 +0200 |
wenzelm |
more method position information, notably finished_pos after end of previous text;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 20:23:00 +0200 |
wenzelm |
more proof method text position information;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 17:47:23 +0200 |
wenzelm |
clarified defer/prefer: more specific errors;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2012 18:04:11 +0200 |
wenzelm |
refined Proof.the_finished_goal with more informative error;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 21:43:59 +0100 |
wenzelm |
canonical argument order for attribute application;
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 19:51:39 +0100 |
wenzelm |
tuned signature, according to actual usage of these operations;
|
file |
diff |
annotate
|