src/Pure/General/name_space.ML
changeset 30522 e26b80647189
parent 30469 de9e8f1d927c
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/General/name_space.ML	Fri Mar 13 23:56:07 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Sat Mar 14 00:13:50 2009 +0100
     1.3 @@ -35,7 +35,6 @@
     1.4    val add_path: string -> naming -> naming
     1.5    val root_path: naming -> naming
     1.6    val parent_path: naming -> naming
     1.7 -  val no_base_names: naming -> naming
     1.8    val mandatory_path: string -> naming -> naming
     1.9    type 'a table = T * 'a Symtab.table
    1.10    val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    1.11 @@ -171,40 +170,22 @@
    1.12  
    1.13  (* datatype naming *)
    1.14  
    1.15 -datatype naming = Naming of
    1.16 - {path: (string * bool) list,
    1.17 -  no_base_names: bool};
    1.18 +datatype naming = Naming of (string * bool) list;
    1.19 +fun map_naming f (Naming path) = Naming (f path);
    1.20  
    1.21 -fun make_naming (path, no_base_names) =
    1.22 -  Naming {path = path, no_base_names = no_base_names};
    1.23 -
    1.24 -fun map_naming f (Naming {path, no_base_names}) =
    1.25 -  make_naming (f (path, no_base_names));
    1.26 -
    1.27 -
    1.28 -(* configure naming *)
    1.29 +val default_naming = Naming [];
    1.30  
    1.31 -val default_naming = make_naming ([], false);
    1.32 -
    1.33 -fun add_path elems = map_naming (fn (path, no_base_names) =>
    1.34 -  (path @ [(elems, false)], no_base_names));
    1.35 -
    1.36 -val root_path = map_naming (fn (_, no_base_names) => ([], no_base_names));
    1.37 -
    1.38 -val parent_path = map_naming (fn (path, no_base_names) =>
    1.39 -  (perhaps (try (#1 o split_last)) path, no_base_names));
    1.40 -
    1.41 -fun mandatory_path elems = map_naming (fn (path, no_base_names) =>
    1.42 -  (path @ [(elems, true)], no_base_names));
    1.43 -
    1.44 -val no_base_names = map_naming (fn (path, _) => (path, true));
    1.45 +fun add_path elems = map_naming (fn path => path @ [(elems, false)]);
    1.46 +val root_path = map_naming (fn _ => []);
    1.47 +val parent_path = map_naming (perhaps (try (#1 o split_last)));
    1.48 +fun mandatory_path elems = map_naming (fn path => path @ [(elems, true)]);
    1.49  
    1.50  
    1.51  (* full name *)
    1.52  
    1.53  fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
    1.54  
    1.55 -fun name_spec (Naming {path, ...}) binding =
    1.56 +fun name_spec (Naming path) binding =
    1.57    let
    1.58      val (prefix, name) = Binding.dest binding;
    1.59      val _ = Long_Name.is_qualified name andalso err_bad binding;
    1.60 @@ -232,16 +213,12 @@
    1.61  
    1.62  fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
    1.63  
    1.64 -fun accesses (naming as Naming {no_base_names, ...}) binding =
    1.65 +fun accesses naming binding =
    1.66    let
    1.67      val spec = name_spec naming binding;
    1.68      val sfxs = mandatory_suffixes spec;
    1.69      val pfxs = mandatory_prefixes spec;
    1.70 -  in
    1.71 -    (sfxs @ pfxs, sfxs)
    1.72 -    |> pairself (no_base_names ? filter (fn [_] => false | _ => true))
    1.73 -    |> pairself (map Long_Name.implode)
    1.74 -  end;
    1.75 +  in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
    1.76  
    1.77  fun external_names naming = #2 o accesses naming o Binding.qualified_name;
    1.78