Tue, 03 Mar 2009 18:32:01 +0100 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;
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;
Tue, 03 Mar 2009 18:31:59 +0100 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
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;
Tue, 03 Mar 2009 17:42:30 +0100 added markup for binding;
wenzelm [Tue, 03 Mar 2009 17:42:30 +0100] rev 30221
added markup for binding; tuned;
Tue, 03 Mar 2009 15:12:52 +0100 Binding.str_of;
wenzelm [Tue, 03 Mar 2009 15:12:52 +0100] rev 30220
Binding.str_of; removed dead code; tuned;
Tue, 03 Mar 2009 15:09:09 +0100 Binding.str_of;
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;
Tue, 03 Mar 2009 15:09:08 +0100 Binding.str_of;
wenzelm [Tue, 03 Mar 2009 15:09:08 +0100] rev 30218
Binding.str_of;
Tue, 03 Mar 2009 15:09:07 +0100 renamed Binding.display to Binding.str_of, which is slightly more canonical;
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;
Tue, 03 Mar 2009 14:54:12 +0100 nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
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;
Tue, 03 Mar 2009 14:53:29 +0100 moved name space externalization flags back to name_space.ML;
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;
Tue, 03 Mar 2009 14:52:13 +0100 moved name space externalization flags back to name_space.ML;
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip