renamed bind to define;
authorwenzelm
Thu Mar 12 11:09:26 2009 +0100 (2009-03-12)
changeset 30465038839f111a1
parent 30464 a858ff86883b
child 30466 5f31e24937c5
renamed bind to define;
misc tuning and polishing;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Thu Mar 12 11:07:22 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 12 11:09:26 2009 +0100
     1.3 @@ -38,11 +38,11 @@
     1.4    val no_base_names: naming -> naming
     1.5    val sticky_prefix: string -> naming -> naming
     1.6    type 'a table = T * 'a Symtab.table
     1.7 -  val bind: naming -> binding * 'a -> 'a table -> string * 'a table       (*exception Symtab.DUP*)
     1.8 +  val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
     1.9    val empty_table: 'a table
    1.10 -  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table  (*exception Symtab.DUP*)
    1.11 +  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception Symtab.DUP*)
    1.12    val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) ->
    1.13 -    'a table * 'a table -> 'a table                                       (*exception Symtab.DUP*)
    1.14 +    'a table * 'a table -> 'a table (*exception Symtab.DUP*)
    1.15    val dest_table: 'a table -> (string * 'a) list
    1.16    val extern_table: 'a table -> (xstring * 'a) list
    1.17  end;
    1.18 @@ -156,8 +156,8 @@
    1.19  fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
    1.20    let
    1.21      val tab' = (tab1, tab2) |> Symtab.join
    1.22 -      (K (fn names as ((names1, names1'), (names2, names2')) =>
    1.23 -        if pointer_eq names then raise Symtab.SAME
    1.24 +      (K (fn ((names1, names1'), (names2, names2')) =>
    1.25 +        if pointer_eq (names1, names2) andalso pointer_eq (names1', names2') then raise Symtab.SAME
    1.26          else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
    1.27      val xtab' = (xtab1, xtab2) |> Symtab.join
    1.28        (K (fn xnames =>
    1.29 @@ -187,7 +187,7 @@
    1.30  val default_naming = make_naming ([], false);
    1.31  
    1.32  fun add_path elems = map_naming (fn (path, no_base_names) =>
    1.33 -  (path @ map (rpair false) (Long_Name.explode elems), 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 @@ -195,14 +195,14 @@
    1.39    (perhaps (try (#1 o split_last)) path, no_base_names));
    1.40  
    1.41  fun sticky_prefix elems = map_naming (fn (path, no_base_names) =>
    1.42 -  (path @ map (rpair true) (Long_Name.explode elems), no_base_names));
    1.43 +  (path @ [(elems, true)], no_base_names));
    1.44  
    1.45  val no_base_names = map_naming (fn (path, _) => (path, true));
    1.46  
    1.47  
    1.48  (* full name *)
    1.49  
    1.50 -fun err_bad binding = error ("Bad name declaration " ^ quote (Binding.str_of binding));
    1.51 +fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
    1.52  
    1.53  fun name_spec (Naming {path, ...}) binding =
    1.54    let
    1.55 @@ -230,7 +230,6 @@
    1.56    | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
    1.57    | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
    1.58  
    1.59 -fun mandatory_suffixes1 xs = map rev (mandatory_prefixes1 (rev xs));
    1.60  fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
    1.61  
    1.62  fun accesses (naming as Naming {no_base_names, ...}) binding =
    1.63 @@ -264,7 +263,7 @@
    1.64  
    1.65  type 'a table = T * 'a Symtab.table;
    1.66  
    1.67 -fun bind naming (binding, x) (space, tab) =
    1.68 +fun define naming (binding, x) (space, tab) =
    1.69    let val (name, space') = declare naming binding space
    1.70    in (name, (space', Symtab.update_new (name, x) tab)) end;
    1.71