src/Pure/General/name_space.ML
changeset 28965 1de908189869
parent 28941 128459bd72d2
child 28991 694227dd3e8c
     1.1 --- a/src/Pure/General/name_space.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -30,27 +30,24 @@
     1.4    val get_accesses: T -> string -> xstring list
     1.5    val merge: T * T -> T
     1.6    type naming
     1.7 -  val path_of: naming -> string
     1.8 +  val default_naming: naming
     1.9 +  val declare: naming -> Binding.T -> T -> string * T
    1.10 +  val full_name: naming -> Binding.T -> string
    1.11 +  val declare_base: naming -> string -> T -> T
    1.12    val external_names: naming -> string -> string list
    1.13 -  val full: naming -> bstring -> string
    1.14 -  val declare: naming -> string -> T -> T
    1.15 -  val default_naming: naming
    1.16 +  val path_of: naming -> string
    1.17    val add_path: string -> naming -> naming
    1.18    val no_base_names: naming -> naming
    1.19    val qualified_names: naming -> naming
    1.20    val sticky_prefix: string -> naming -> naming
    1.21 -  val full_binding: naming -> Binding.T -> string
    1.22 -  val declare_binding: naming -> Binding.T -> T -> string * T
    1.23    type 'a table = T * 'a Symtab.table
    1.24    val empty_table: 'a table
    1.25 -  val table_declare: naming -> Binding.T * 'a
    1.26 +  val bind: naming -> Binding.T * 'a
    1.27      -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    1.28 -  val table_declare_permissive: naming -> Binding.T * 'a
    1.29 -    -> 'a table -> string * 'a table
    1.30 -  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    1.31    val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    1.32    val dest_table: 'a table -> (string * 'a) list
    1.33    val extern_table: 'a table -> (xstring * 'a) list
    1.34 +  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    1.35  end;
    1.36  
    1.37  structure NameSpace: NAME_SPACE =
    1.38 @@ -269,7 +266,11 @@
    1.39  
    1.40  fun full (Naming (path, (qualify, _))) = qualify path;
    1.41  
    1.42 -fun declare naming name space =
    1.43 +fun full_name naming b =
    1.44 +  let val (prefix, bname) = Binding.dest b
    1.45 +  in full (apply_prefix prefix naming) bname end;
    1.46 +
    1.47 +fun declare_base naming name space =
    1.48    if is_hidden name then
    1.49      error ("Attempt to declare hidden name " ^ quote name)
    1.50    else
    1.51 @@ -281,12 +282,12 @@
    1.52        val (accs, accs') = pairself (map implode_name) (accesses naming names);
    1.53      in space |> fold (add_name name) accs |> put_accesses name accs' end;
    1.54  
    1.55 -fun declare_binding bnaming b =
    1.56 +fun declare bnaming b =
    1.57    let
    1.58 -    val (prefix, bname) = Binding.dest_binding b;
    1.59 +    val (prefix, bname) = Binding.dest b;
    1.60      val naming = apply_prefix prefix bnaming;
    1.61      val name = full naming bname;
    1.62 -  in declare naming name #> pair name end;
    1.63 +  in declare_base naming name #> pair name end;
    1.64  
    1.65  
    1.66  
    1.67 @@ -296,21 +297,14 @@
    1.68  
    1.69  val empty_table = (empty, Symtab.empty);
    1.70  
    1.71 -fun gen_table_declare update naming (binding, x) (space, tab) =
    1.72 +fun bind naming (b, x) (space, tab) =
    1.73    let
    1.74 -    val (name, space') = declare_binding naming binding space;
    1.75 -  in (name, (space', update (name, x) tab)) end;
    1.76 -
    1.77 -fun table_declare naming = gen_table_declare Symtab.update_new naming;
    1.78 -fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
    1.79 -
    1.80 -fun full_binding naming b =
    1.81 -  let val (prefix, bname) = Binding.dest_binding b
    1.82 -  in full (apply_prefix prefix naming) bname end;
    1.83 +    val (name, space') = declare naming b space;
    1.84 +  in (name, (space', Symtab.update_new (name, x) tab)) end;
    1.85  
    1.86  fun extend_table naming bentries (space, tab) =
    1.87    let val entries = map (apfst (full naming)) bentries
    1.88 -  in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
    1.89 +  in (fold (declare_base naming o #1) entries space, Symtab.extend (tab, entries)) end;
    1.90  
    1.91  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
    1.92    (merge (space1, space2), Symtab.merge eq (tab1, tab2));