2011-07-15 ago more robust Binding.pretty/print in typical error sitations with spaces etc. (NB: markup can only provide *additional* emphasis and is occasionally suppressed in TTY mode or tooltips);
2011-07-15 ago more visible printing of empty binding;
2011-06-25 ago clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
2011-06-25 ago clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example;
2011-04-17 ago added Binding.print convenience, which includes quote already;
2010-12-17 ago extra checking of name bindings for classes, types, consts;
2010-09-17 ago tuned;
2010-02-18 ago more systematic treatment of qualified names derived from binding;
2009-10-25 ago allow name space entries to be "concealed" -- via binding/naming/local_theory;
2009-09-16 ago replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
2009-03-30 ago qualified_name_of: observe empty case;
2009-03-12 ago tuned signature;
2009-03-10 ago added qualified_name_of;
2009-03-08 ago added qualified_name -- emulates old-style qualified bstring;
2009-03-07 ago added prefix_name, suffix_name;
2009-03-07 ago Binding.str_of: removed verbose feature, include qualifier in output;
2009-03-05 ago added prefix_of;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago tuned str_of, now subject to verbose flag;
2009-03-03 ago moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
2009-03-03 ago renamed Binding.display to Binding.str_of, which is slightly more canonical;
2009-03-03 ago moved name space externalization flags back to name_space.ML;
2009-01-22 ago tuned signature;
2009-01-21 ago binding is alias for Binding.T
2009-01-03 ago separator, is_qualified
2008-12-10 ago Use prefix component of bindings for locale prefixes.
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-12-01 ago new Binding module