src/Pure/General/name_space.ML
changeset 28991 694227dd3e8c
parent 28965 1de908189869
child 29004 a5a91f387791
     1.1 --- a/src/Pure/General/name_space.ML	Thu Dec 04 14:44:07 2008 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Fri Dec 05 08:04:53 2008 +0100
     1.3 @@ -33,7 +33,6 @@
     1.4    val default_naming: naming
     1.5    val declare: naming -> Binding.T -> T -> string * T
     1.6    val full_name: naming -> Binding.T -> string
     1.7 -  val declare_base: naming -> string -> T -> T
     1.8    val external_names: naming -> string -> string list
     1.9    val path_of: naming -> string
    1.10    val add_path: string -> naming -> naming
    1.11 @@ -45,6 +44,8 @@
    1.12    val bind: naming -> Binding.T * 'a
    1.13      -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    1.14    val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    1.15 +  val join_tables: (string -> 'a * 'a -> 'a)
    1.16 +    -> 'a table * 'a table -> 'a table
    1.17    val dest_table: 'a table -> (string * 'a) list
    1.18    val extern_table: 'a table -> (xstring * 'a) list
    1.19    val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    1.20 @@ -264,13 +265,9 @@
    1.21  
    1.22  (* declarations *)
    1.23  
    1.24 -fun full (Naming (path, (qualify, _))) = qualify path;
    1.25 +fun full_internal (Naming (path, (qualify, _))) = qualify path;
    1.26  
    1.27 -fun full_name naming b =
    1.28 -  let val (prefix, bname) = Binding.dest b
    1.29 -  in full (apply_prefix prefix naming) bname end;
    1.30 -
    1.31 -fun declare_base naming name space =
    1.32 +fun declare_internal naming name space =
    1.33    if is_hidden name then
    1.34      error ("Attempt to declare hidden name " ^ quote name)
    1.35    else
    1.36 @@ -282,12 +279,16 @@
    1.37        val (accs, accs') = pairself (map implode_name) (accesses naming names);
    1.38      in space |> fold (add_name name) accs |> put_accesses name accs' end;
    1.39  
    1.40 +fun full_name naming b =
    1.41 +  let val (prefix, bname) = Binding.dest b
    1.42 +  in full_internal (apply_prefix prefix naming) bname end;
    1.43 +
    1.44  fun declare bnaming b =
    1.45    let
    1.46      val (prefix, bname) = Binding.dest b;
    1.47      val naming = apply_prefix prefix bnaming;
    1.48 -    val name = full naming bname;
    1.49 -  in declare_base naming name #> pair name end;
    1.50 +    val name = full_internal naming bname;
    1.51 +  in declare_internal naming name #> pair name end;
    1.52  
    1.53  
    1.54  
    1.55 @@ -303,12 +304,15 @@
    1.56    in (name, (space', Symtab.update_new (name, x) tab)) end;
    1.57  
    1.58  fun extend_table naming bentries (space, tab) =
    1.59 -  let val entries = map (apfst (full naming)) bentries
    1.60 -  in (fold (declare_base naming o #1) entries space, Symtab.extend (tab, entries)) end;
    1.61 +  let val entries = map (apfst (full_internal naming)) bentries
    1.62 +  in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
    1.63  
    1.64  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
    1.65    (merge (space1, space2), Symtab.merge eq (tab1, tab2));
    1.66  
    1.67 +fun join_tables f ((space1, tab1), (space2, tab2)) =
    1.68 +  (merge (space1, space2), Symtab.join f (tab1, tab2));
    1.69 +
    1.70  fun ext_table (space, tab) =
    1.71    Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
    1.72    |> Library.sort_wrt (#2 o #1);