src/Pure/Isar/proof_context.ML
Wed, 02 Jul 2014 12:12:26 +0200 wenzelm check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
Fri, 27 Jun 2014 16:04:56 +0200 wenzelm command 'print_term_bindings' supersedes 'print_binds';
Mon, 05 May 2014 16:30:19 +0200 wenzelm more print operations;
Mon, 05 May 2014 15:17:07 +0200 wenzelm support print operations as asynchronous query;
Sun, 06 Apr 2014 16:36:28 +0200 wenzelm more source positions;
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
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;
Wed, 26 Mar 2014 14:41:52 +0100 wenzelm prefer Context_Position where a context is available;
Tue, 18 Mar 2014 12:25:17 +0100 wenzelm more markup for improper elements;
Sat, 15 Mar 2014 11:22:25 +0100 wenzelm more explicit treatment of verbose mode, which includes concealed entries;
Sat, 15 Mar 2014 10:24:49 +0100 wenzelm clarified retrieve_generic: local error takes precedence, which is relevant for completion;
Sat, 15 Mar 2014 10:14:42 +0100 wenzelm clarified print_local_facts;
Fri, 14 Mar 2014 15:26:52 +0100 wenzelm conceal improper cases, e.g. relevant for completion (and potentially for markup);
Fri, 14 Mar 2014 14:59:43 +0100 wenzelm more accurate resolution of hybrid facts, which actually changes the sort order of results;
Fri, 14 Mar 2014 12:23:59 +0100 wenzelm back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
Fri, 14 Mar 2014 10:08:36 +0100 wenzelm just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
Thu, 13 Mar 2014 17:26:22 +0100 wenzelm more frugal recording of changes: join merely requires information from one side;
Wed, 12 Mar 2014 14:37:14 +0100 wenzelm tuned signature;
Tue, 11 Mar 2014 14:28:39 +0100 wenzelm tuned signature;
Mon, 10 Mar 2014 22:39:37 +0100 wenzelm tuned message;
Mon, 10 Mar 2014 22:28:20 +0100 wenzelm tuned message;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Sun, 09 Mar 2014 17:40:02 +0100 wenzelm tuned;
Sun, 09 Mar 2014 16:37:56 +0100 wenzelm tuned signature;
Thu, 06 Mar 2014 17:37:32 +0100 wenzelm more decisive commitment to get_free vs. the_const;
Thu, 06 Mar 2014 16:12:26 +0100 wenzelm reject internal term names outright, and complete consts instead;
Thu, 06 Mar 2014 14:38:54 +0100 wenzelm eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
Thu, 06 Mar 2014 13:44:01 +0100 wenzelm more uniform check_const/read_const;
Thu, 06 Mar 2014 12:10:19 +0100 wenzelm tuned signature -- more uniform check_type_name/read_type_name;
Thu, 06 Mar 2014 11:32:16 +0100 wenzelm clarified treatment of consts -- prefer value-oriented reports;
less more (0) -300 -100 -50 -30 tip