diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 7 | ||||
| -rw-r--r-- | kernel/names.mli | 5 |
2 files changed, 7 insertions, 5 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 0209d1c33d..b67fd32ad5 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -71,7 +71,7 @@ let string_of_dirpath = function let u_number = ref 0 type uniq_ident = int * string * dir_path -let make_uid dir s = incr u_number;(!u_number,s,dir) +let make_uid dir s = incr u_number;(!u_number,String.copy s,dir) let string_of_uid (i,s,p) = "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" @@ -83,11 +83,12 @@ module Umap = Map.Make(struct type mod_self_id = uniq_ident let make_msid = make_uid -let string_of_msid = string_of_uid +let debug_string_of_msid = string_of_uid type mod_bound_id = uniq_ident let make_mbid = make_uid -let string_of_mbid = string_of_uid +let debug_string_of_mbid = string_of_uid +let id_of_mbid (_,s,_) = s type label = string let mk_label l = l diff --git a/kernel/names.mli b/kernel/names.mli index b1bcc0b83b..d9b9ddc9cd 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -48,13 +48,14 @@ type mod_self_id (* The first argument is a file name - to prevent conflict between different files *) val make_msid : dir_path -> string -> mod_self_id -val string_of_msid : mod_self_id -> string +val debug_string_of_msid : mod_self_id -> string (*s Unique names for bound modules *) type mod_bound_id val make_mbid : dir_path -> string -> mod_bound_id -val string_of_mbid : mod_bound_id -> string +val id_of_mbid : mod_bound_id -> identifier +val debug_string_of_mbid : mod_bound_id -> string (*s Names of structure elements *) type label |