removed qualified_force_prefix;
authorwenzelm
Wed Feb 15 21:35:06 2006 +0100 (2006-02-15)
changeset 190554f408867f9d4
parent 19054 af7cc6063285
child 19056 6ac9dfe98e54
removed qualified_force_prefix;
added sticky_prefix;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Wed Feb 15 21:35:04 2006 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Feb 15 21:35:06 2006 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4    val add_path: string -> naming -> naming
     1.5    val no_base_names: naming -> naming
     1.6    val qualified_names: naming -> naming
     1.7 -  val qualified_force_prefix: string -> naming -> naming
     1.8 +  val sticky_prefix: string -> naming -> naming
     1.9    val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    1.10      naming -> naming
    1.11    type 'a table (*= T * 'a Symtab.table*)
    1.12 @@ -256,9 +256,9 @@
    1.13  
    1.14  fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
    1.15  
    1.16 -fun qualified_force_prefix prfx (Naming (path, _)) =
    1.17 -  Naming (path,
    1.18 -    (qualified, suffixes_prefixes_split (length (unpack path)) (length (unpack prfx))));
    1.19 +fun sticky_prefix prfx (Naming (path, (qualify, _))) =
    1.20 +  Naming (append path prfx,
    1.21 +    (qualify, suffixes_prefixes_split (length (unpack path)) (length (unpack prfx))));
    1.22  
    1.23  fun set_policy policy (Naming (path, _)) = Naming (path, policy);
    1.24