added flag unique_names
authorschirmer
Tue Jul 06 20:31:37 2004 +0200 (2004-07-06)
changeset 15016bcbef8418da5
parent 15015 c5768e8c4da4
child 15017 9ad392226da5
added flag unique_names
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Tue Jul 06 20:31:06 2004 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Jul 06 20:31:37 2004 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    val extern: T -> string -> string
     1.5    val long_names: bool ref
     1.6    val short_names: bool ref
     1.7 +  val unique_names: bool ref
     1.8    val cond_extern: T -> string -> string
     1.9    val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list
    1.10    val dest: T -> (string * string list) list
    1.11 @@ -140,20 +141,25 @@
    1.12  
    1.13  fun intern spc xname = #1 (lookup spc xname);
    1.14  
    1.15 -fun extern space name =
    1.16 +fun unique_extern mkunique space name =
    1.17    let
    1.18      fun try [] = hidden name
    1.19        | try (nm :: nms) =
    1.20            let val (full_nm, uniq) = lookup space nm
    1.21 -          in if full_nm = name andalso uniq then nm else try nms end
    1.22 +          in if full_nm = name andalso (uniq orelse (not mkunique)) then nm else try nms end
    1.23    in try (accesses' name) end;
    1.24  
    1.25 +(*output unique names by default*)
    1.26 +val unique_names = ref true;
    1.27 +
    1.28  (*prune names on output by default*)
    1.29  val long_names = ref false;
    1.30  
    1.31  (*output only base name*)
    1.32  val short_names = ref false;
    1.33  
    1.34 +fun extern space name = unique_extern (!unique_names) space name; 
    1.35 +
    1.36  fun cond_extern space =
    1.37    if ! long_names then I
    1.38    else if ! short_names then base else extern space;