| Sun, 29 Mar 2015 19:23:08 +0200 |
wenzelm |
proper local Proof_Context.arity_sorts;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 11:53:18 +0100 |
wenzelm |
clarified input source;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 13:28:04 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2015 23:35:41 +0100 |
wenzelm |
added Proof_Context.cterm_of/ctyp_of convenience;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 17:23:56 +0100 |
wenzelm |
more frugal Local_Syntax.init -- maintain idents within context;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 13:15:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 22:43:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 20 Aug 2014 11:51:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 16:20:14 +0200 |
wenzelm |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 14:57:03 +0200 |
wenzelm |
transfer result of Global_Theory.add_thms_dynamic to context stack;
|
file |
diff |
annotate
|
| Sun, 10 Aug 2014 19:44:20 +0200 |
wenzelm |
support aliases within the facts space;
|
file |
diff |
annotate
|
| Wed, 02 Jul 2014 12:12:26 +0200 |
wenzelm |
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 16:04:56 +0200 |
wenzelm |
command 'print_term_bindings' supersedes 'print_binds';
|
file |
diff |
annotate
|
| Mon, 05 May 2014 16:30:19 +0200 |
wenzelm |
more print operations;
|
file |
diff |
annotate
|
| Mon, 05 May 2014 15:17:07 +0200 |
wenzelm |
support print operations as asynchronous query;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
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
|
| Mon, 31 Mar 2014 10:28:08 +0200 |
wenzelm |
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;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 14:41:52 +0100 |
wenzelm |
prefer Context_Position where a context is available;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 12:25:17 +0100 |
wenzelm |
more markup for improper elements;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 11:22:25 +0100 |
wenzelm |
more explicit treatment of verbose mode, which includes concealed entries;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 10:24:49 +0100 |
wenzelm |
clarified retrieve_generic: local error takes precedence, which is relevant for completion;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 10:14:42 +0100 |
wenzelm |
clarified print_local_facts;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 15:26:52 +0100 |
wenzelm |
conceal improper cases, e.g. relevant for completion (and potentially for markup);
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 14:59:43 +0100 |
wenzelm |
more accurate resolution of hybrid facts, which actually changes the sort order of results;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 12:23:59 +0100 |
wenzelm |
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 10:08:36 +0100 |
wenzelm |
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 17:26:22 +0100 |
wenzelm |
more frugal recording of changes: join merely requires information from one side;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 14:37:14 +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 22:39:37 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 22:28:20 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 17:40:02 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 16:37:56 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 17:37:32 +0100 |
wenzelm |
more decisive commitment to get_free vs. the_const;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 16:12:26 +0100 |
wenzelm |
reject internal term names outright, and complete consts instead;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:38:54 +0100 |
wenzelm |
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:44:01 +0100 |
wenzelm |
more uniform check_const/read_const;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:10:19 +0100 |
wenzelm |
tuned signature -- more uniform check_type_name/read_type_name;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 11:32:16 +0100 |
wenzelm |
clarified treatment of consts -- prefer value-oriented reports;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 10:53:14 +0100 |
wenzelm |
clarified check of internal names;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 10:12:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 19:52:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 18:26:35 +0100 |
wenzelm |
more markup for inner syntax class/type names (notably for completion);
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 21:30:47 +0100 |
wenzelm |
prefer Name_Space.check with its builtin reports (including completion);
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 21:13:29 +0100 |
wenzelm |
tuned source structure;
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 21:02:27 +0100 |
wenzelm |
prefer Name_Space.check with its builtin reports (including completion);
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 20:34:11 +0100 |
wenzelm |
consider completion report as part of error message -- less stateful, may get handled;
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 20:20:20 +0100 |
wenzelm |
more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 23:17:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 11:36:04 +0100 |
wenzelm |
more positions;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 14:58:40 +0100 |
wenzelm |
prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 16:33:54 +0100 |
wenzelm |
more formal markup;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|