src/Pure/General/name_space.ML
changeset 19015 1075db658d91
parent 18939 18e2a2676d80
child 19030 78d43fe9ac65
     1.1 --- a/src/Pure/General/name_space.ML	Sat Feb 11 17:17:49 2006 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Sat Feb 11 17:17:50 2006 +0100
     1.3 @@ -30,6 +30,7 @@
     1.4    val drop_base: string -> string
     1.5    val map_base: (string -> string) -> string -> string
     1.6    val suffixes_prefixes: 'a list -> 'a list list
     1.7 +  val suffixes_prefixes_split: int -> int -> 'a list -> 'a list list
     1.8    val accesses: string -> string list
     1.9    val accesses': string -> string list
    1.10    type T
    1.11 @@ -45,9 +46,9 @@
    1.12    val declare: naming -> string -> T -> T
    1.13    val default_naming: naming
    1.14    val add_path: string -> naming -> naming
    1.15 +  val no_base_names: naming -> naming
    1.16    val qualified_names: naming -> naming
    1.17 -  val no_base_names: naming -> naming
    1.18 -  val custom_accesses: (string list -> string list list) -> naming -> naming
    1.19 +  val qualified_force_prefix: string -> naming -> naming
    1.20    val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    1.21      naming -> naming
    1.22    type 'a table (*= T * 'a Symtab.table*)
    1.23 @@ -91,11 +92,29 @@
    1.24        let val names = unpack name
    1.25        in pack (nth_map (length names - 1) f names) end;
    1.26  
    1.27 -fun suffixes_prefixes xs =
    1.28 +
    1.29 +(* accesses *)
    1.30 +
    1.31 +infixr 6 @@;
    1.32 +fun ([] @@ yss) = []
    1.33 +  | ((xs :: xss) @@ yss) = map (fn ys => xs @ ys) yss @ (xss @@ yss);
    1.34 +
    1.35 +fun suffixes_prefixes list =
    1.36    let
    1.37 -    val (qs, b) = split_last xs;
    1.38 -    val sfxs = Library.suffixes1 xs;
    1.39 -    val pfxs = map (fn x => x @ [b]) (Library.prefixes1 qs);
    1.40 +    val (xs, ws) = chop (length list - 1) list;
    1.41 +    val sfxs = suffixes xs @@ [ws];
    1.42 +    val pfxs = prefixes1 xs @@ [ws];
    1.43 +  in sfxs @ pfxs end;
    1.44 +
    1.45 +fun suffixes_prefixes_split i k list =
    1.46 +  let
    1.47 +    val (((xs, ys), zs), ws) = list |> chop i ||>> chop k ||>> chop (length list - (i + k + 1));
    1.48 +    val sfxs =
    1.49 +      [ys] @@ suffixes zs @@ [ws] @
    1.50 +      suffixes1 xs @@ [ys @ zs @ ws];
    1.51 +    val pfxs =
    1.52 +      prefixes1 xs @@ [ys @ ws] @
    1.53 +      [xs @ ys] @@ prefixes1 zs @@ [ws];
    1.54    in sfxs @ pfxs end;
    1.55  
    1.56  val accesses = map pack o suffixes_prefixes o unpack;
    1.57 @@ -224,12 +243,15 @@
    1.58    else if elems = ".." then Naming (drop_base path, policy)
    1.59    else Naming (append path elems, policy);
    1.60  
    1.61 -fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
    1.62 -
    1.63  fun no_base_names (Naming (path, (qualify, accs))) =
    1.64    Naming (path, (qualify, filter_out (fn [_] => true | _ => false) o accs));
    1.65  
    1.66 -fun custom_accesses accs (Naming (path, (qualify, _))) = Naming (path, (qualify, accs));
    1.67 +fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
    1.68 +
    1.69 +fun qualified_force_prefix prfx (Naming (path, _)) =
    1.70 +  Naming (path,
    1.71 +    (qualified, suffixes_prefixes_split (length (unpack path)) (length (unpack prfx))));
    1.72 +
    1.73  fun set_policy policy (Naming (path, _)) = Naming (path, policy);
    1.74  
    1.75