wenzelm [Tue, 03 Mar 2009 19:30:43 +0100] rev 30229
merged
haftmann [Tue, 03 Mar 2009 19:21:10 +0100] rev 30228
merged
haftmann [Tue, 03 Mar 2009 13:20:53 +0100] rev 30227
tuned manuals
haftmann [Tue, 03 Mar 2009 11:00:51 +0100] rev 30226
more canonical directory structure of manuals
wenzelm [Tue, 03 Mar 2009 18:33:21 +0100] rev 30225
merged
nipkow [Tue, 03 Mar 2009 17:05:18 +0100] rev 30224
removed and renamed redundant lemmas
wenzelm [Tue, 03 Mar 2009 18:32:01 +0100] rev 30223
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
minor tuning;
wenzelm [Tue, 03 Mar 2009 18:31:59 +0100] rev 30222
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names;
type binding: maintain explicit qualifier, indepently of base name;
tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused);
Binding.str_of: include markup with position properties;
misc tuning;
wenzelm [Tue, 03 Mar 2009 17:42:30 +0100] rev 30221
added markup for binding;
tuned;
wenzelm [Tue, 03 Mar 2009 15:12:52 +0100] rev 30220
Binding.str_of;
removed dead code;
tuned;
wenzelm [Tue, 03 Mar 2009 15:09:09 +0100] rev 30219
Binding.str_of;
pretty_name_atts: check Binding.is_empty, not result of Binding.str_of;
wenzelm [Tue, 03 Mar 2009 15:09:08 +0100] rev 30218
Binding.str_of;
wenzelm [Tue, 03 Mar 2009 15:09:07 +0100] rev 30217
renamed Binding.display to Binding.str_of, which is slightly more canonical;
tuned signature;
wenzelm [Tue, 03 Mar 2009 14:54:12 +0100] rev 30216
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm [Tue, 03 Mar 2009 14:53:29 +0100] rev 30215
moved name space externalization flags back to name_space.ML;
added pure version extern_flags;
do not export internal get_accesses;
wenzelm [Tue, 03 Mar 2009 14:52:13 +0100] rev 30214
moved name space externalization flags back to name_space.ML;
display: always show prefix for now;
tuned signature;
wenzelm [Tue, 03 Mar 2009 14:16:05 +0100] rev 30213
reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
wenzelm [Tue, 03 Mar 2009 14:08:53 +0100] rev 30212
merged
wenzelm [Tue, 03 Mar 2009 14:07:43 +0100] rev 30211
Thm.binding;
wenzelm [Tue, 03 Mar 2009 14:07:23 +0100] rev 30210
added type binding and val empty_binding;
wenzelm [Tue, 03 Mar 2009 13:22:01 +0100] rev 30209
updated generated files;
wenzelm [Tue, 03 Mar 2009 12:12:38 +0100] rev 30208
ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;
Timothy Bourke [Tue, 03 Mar 2009 12:14:52 +1100] rev 30207
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke [Mon, 02 Mar 2009 18:11:39 +1100] rev 30206
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
wenzelm [Mon, 02 Mar 2009 20:31:27 +0100] rev 30205
adapted to lates experimental version;
PolyML.Compiler.CPPrintInAlphabeticalOrder false (redundant?);
wenzelm [Mon, 02 Mar 2009 20:29:43 +0100] rev 30204
removed Ids;
haftmann [Mon, 02 Mar 2009 18:50:41 +0100] rev 30203
merged
haftmann [Mon, 02 Mar 2009 16:58:39 +0100] rev 30202
reduced confusion code_funcgr vs. code_wellsorted