| Tue, 03 Mar 2009 18:32:01 +0100 |
wenzelm |
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;
|
changeset |
files
|
| Tue, 03 Mar 2009 18:31:59 +0100 |
wenzelm |
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
|
changeset |
files
|
| Tue, 03 Mar 2009 17:42:30 +0100 |
wenzelm |
added markup for binding;
|
changeset |
files
|
| Tue, 03 Mar 2009 15:12:52 +0100 |
wenzelm |
Binding.str_of;
|
changeset |
files
|
| Tue, 03 Mar 2009 15:09:09 +0100 |
wenzelm |
Binding.str_of;
|
changeset |
files
|
| Tue, 03 Mar 2009 15:09:08 +0100 |
wenzelm |
Binding.str_of;
|
changeset |
files
|
| Tue, 03 Mar 2009 15:09:07 +0100 |
wenzelm |
renamed Binding.display to Binding.str_of, which is slightly more canonical;
|
changeset |
files
|
| Tue, 03 Mar 2009 14:54:12 +0100 |
wenzelm |
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
|
changeset |
files
|
| Tue, 03 Mar 2009 14:53:29 +0100 |
wenzelm |
moved name space externalization flags back to name_space.ML;
|
changeset |
files
|
| Tue, 03 Mar 2009 14:52:13 +0100 |
wenzelm |
moved name space externalization flags back to name_space.ML;
|
changeset |
files
|
| Tue, 03 Mar 2009 14:16:05 +0100 |
wenzelm |
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);
|
changeset |
files
|
| Tue, 03 Mar 2009 14:08:53 +0100 |
wenzelm |
merged
|
changeset |
files
|