# HG changeset patch # User schirmer # Date 1089138697 -7200 # Node ID bcbef8418da506db4bd9675beb40e931f735fe45 # Parent c5768e8c4da4df89c83ea8808277a6135a2ed2b2 added flag unique_names diff -r c5768e8c4da4 -r bcbef8418da5 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Tue Jul 06 20:31:06 2004 +0200 +++ b/src/Pure/General/name_space.ML Tue Jul 06 20:31:37 2004 +0200 @@ -30,6 +30,7 @@ val extern: T -> string -> string val long_names: bool ref val short_names: bool ref + val unique_names: bool ref val cond_extern: T -> string -> string val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list val dest: T -> (string * string list) list @@ -140,20 +141,25 @@ fun intern spc xname = #1 (lookup spc xname); -fun extern space name = +fun unique_extern mkunique space name = let fun try [] = hidden name | try (nm :: nms) = let val (full_nm, uniq) = lookup space nm - in if full_nm = name andalso uniq then nm else try nms end + in if full_nm = name andalso (uniq orelse (not mkunique)) then nm else try nms end in try (accesses' name) end; +(*output unique names by default*) +val unique_names = ref true; + (*prune names on output by default*) val long_names = ref false; (*output only base name*) val short_names = ref false; +fun extern space name = unique_extern (!unique_names) space name; + fun cond_extern space = if ! long_names then I else if ! short_names then base else extern space;