src/Pure/General/name_space.ML
changeset 5175 2dbef0104bcf
parent 5012 086b055c4d73
child 5682 9125611c1645
equal deleted inserted replaced
5174:c51961c75921 5175:2dbef0104bcf
    22   val empty: T
    22   val empty: T
    23   val extend: T * string list -> T
    23   val extend: T * string list -> T
    24   val merge: T * T -> T
    24   val merge: T * T -> T
    25   val intern: T -> string -> string
    25   val intern: T -> string -> string
    26   val extern: T -> string -> string
    26   val extern: T -> string -> string
       
    27   val long_names: bool ref
       
    28   val cond_extern: T -> string -> string
    27   val dest: T -> (string * string list) list
    29   val dest: T -> (string * string list) list
    28 end;
    30 end;
    29 
    31 
    30 structure NameSpace: NAME_SPACE =
    32 structure NameSpace: NAME_SPACE =
    31 struct
    33 struct
    94       | try (nm :: nms) =
    96       | try (nm :: nms) =
    95           if intern space nm = name then nm
    97           if intern space nm = name then nm
    96           else try nms;
    98           else try nms;
    97   in try (map pack (suffixes1 (unpack name))) end;
    99   in try (map pack (suffixes1 (unpack name))) end;
    98 
   100 
       
   101 (*prune names on output by default*)
       
   102 val long_names = ref false;
       
   103 
       
   104 fun cond_extern space = if ! long_names then I else extern space;
       
   105 
    99 
   106 
   100 (* dest *)
   107 (* dest *)
   101 
   108 
   102 fun dest (NameSpace tab) =
   109 fun dest (NameSpace tab) =
   103   map (apsnd (sort (int_ord o pairself size)))
   110   map (apsnd (sort (int_ord o pairself size)))
   104     (Symtab.dest (Symtab.make_multi (map swap (Symtab.dest tab))));
   111     (Symtab.dest (Symtab.make_multi (map swap (Symtab.dest tab))));
   105 
   112 
   106 
   113 
   107 end;
   114 end;
       
   115 
       
   116 
       
   117 val long_names = NameSpace.long_names;