moved name space externalization flags back to name_space.ML;
authorwenzelm
Tue Mar 03 14:53:29 2009 +0100 (2009-03-03)
changeset 3021547cce3d47e62
parent 30214 f84c9f10292a
child 30216 0300b7420b07
moved name space externalization flags back to name_space.ML;
added pure version extern_flags;
do not export internal get_accesses;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Tue Mar 03 14:52:13 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 03 14:53:29 2009 +0100
     1.3 @@ -9,9 +9,16 @@
     1.4  type bstring = string;    (*simple names to be bound -- legacy*)
     1.5  type xstring = string;    (*external names*)
     1.6  
     1.7 +signature BASIC_NAME_SPACE =
     1.8 +sig
     1.9 +  val long_names: bool ref
    1.10 +  val short_names: bool ref
    1.11 +  val unique_names: bool ref
    1.12 +end;
    1.13 +
    1.14  signature NAME_SPACE =
    1.15  sig
    1.16 -  include BASIC_BINDING
    1.17 +  include BASIC_NAME_SPACE
    1.18    val hidden: string -> string
    1.19    val is_hidden: string -> bool
    1.20    val separator: string                 (*single char*)
    1.21 @@ -27,8 +34,9 @@
    1.22    val empty: T
    1.23    val intern: T -> xstring -> string
    1.24    val extern: T -> string -> xstring
    1.25 +  val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
    1.26 +    T -> string -> xstring
    1.27    val hide: bool -> string -> T -> T
    1.28 -  val get_accesses: T -> string -> xstring list
    1.29    val merge: T * T -> T
    1.30    type naming
    1.31    val default_naming: naming
    1.32 @@ -54,9 +62,6 @@
    1.33  structure NameSpace: NAME_SPACE =
    1.34  struct
    1.35  
    1.36 -open Basic_Binding;
    1.37 -
    1.38 -
    1.39  (** long identifiers **)
    1.40  
    1.41  fun hidden name = "??." ^ name;
    1.42 @@ -149,20 +154,30 @@
    1.43  
    1.44  fun intern space xname = #1 (lookup space xname);
    1.45  
    1.46 -fun extern space name =
    1.47 +fun extern_flags {long_names, short_names, unique_names} space name =
    1.48    let
    1.49      fun valid unique xname =
    1.50        let val (name', uniq) = lookup space xname
    1.51        in name = name' andalso (uniq orelse not unique) end;
    1.52  
    1.53      fun ext [] = if valid false name then name else hidden name
    1.54 -      | ext (nm :: nms) = if valid (! unique_names) nm then nm else ext nms;
    1.55 +      | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
    1.56    in
    1.57 -    if ! long_names then name
    1.58 -    else if ! short_names then base name
    1.59 +    if long_names then name
    1.60 +    else if short_names then base name
    1.61      else ext (get_accesses space name)
    1.62    end;
    1.63  
    1.64 +val long_names = ref false;
    1.65 +val short_names = ref false;
    1.66 +val unique_names = ref true;
    1.67 +
    1.68 +fun extern space name =
    1.69 +  extern_flags
    1.70 +   {long_names = ! long_names,
    1.71 +    short_names = ! short_names,
    1.72 +    unique_names = ! unique_names} space name;
    1.73 +
    1.74  
    1.75  (* basic operations *)
    1.76  
    1.77 @@ -322,3 +337,7 @@
    1.78  val explode = explode_name;
    1.79  
    1.80  end;
    1.81 +
    1.82 +structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
    1.83 +open BasicNameSpace;
    1.84 +