--- a/src/Pure/General/name_space.ML Thu Nov 20 10:29:35 2008 +0100
+++ b/src/Pure/General/name_space.ML Thu Nov 20 14:51:40 2008 +0100
@@ -16,6 +16,19 @@
val unique_names: bool ref
end;
+signature NAME_BINDING =
+sig
+ type binding
+ val binding_pos: string * Position.T -> binding
+ val binding: string -> binding
+ val no_binding: binding
+ val dest_binding: binding -> (string * bool) list * string
+ val is_nothing: binding -> bool
+ val pos_of: binding -> Position.T
+ val map_binding: ((string * bool) list * string -> (string * bool) list * string)
+ -> binding -> binding
+end
+
signature NAME_SPACE =
sig
include BASIC_NAME_SPACE
@@ -46,8 +59,15 @@
val no_base_names: naming -> naming
val qualified_names: naming -> naming
val sticky_prefix: string -> naming -> naming
+ include NAME_BINDING
+ val full_binding: naming -> binding -> string
+ val declare_binding: naming -> binding -> T -> string * T
type 'a table = T * 'a Symtab.table
val empty_table: 'a table
+ val table_declare: naming -> binding * 'a
+ -> 'a table -> string * 'a table (*exception Symtab.DUP*)
+ val table_declare_permissive: naming -> binding * 'a
+ -> 'a table -> string * 'a table
val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
val dest_table: 'a table -> (string * 'a) list
@@ -220,6 +240,23 @@
+(** generic name bindings **)
+
+datatype binding = Binding of ((string * bool) list * string) * Position.T;
+
+fun binding_pos (name, pos) = Binding (([], name), pos);
+fun binding name = binding_pos (name, Position.none);
+val no_binding = binding "";
+
+fun pos_of (Binding (_, pos)) = pos;
+fun dest_binding (Binding (prefix_name, _)) = prefix_name;
+
+fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
+
+fun is_nothing (Binding ((_, name), _)) = name = "";
+
+
+
(** naming contexts **)
(* datatype naming *)
@@ -235,23 +272,6 @@
fun external_names naming = map implode_name o #2 o accesses naming o explode_name;
-(* declarations *)
-
-fun full (Naming (path, (qualify, _))) = qualify path;
-
-fun declare naming name space =
- if is_hidden name then
- error ("Attempt to declare hidden name " ^ quote name)
- else
- let
- val names = explode_name name;
- val _ = (null names orelse exists (fn s => s = "") names
- orelse exists_string (fn s => s = "\"") name) andalso
- error ("Bad name declaration " ^ quote name);
- val (accs, accs') = pairself (map implode_name) (accesses naming names);
- in space |> fold (add_name name) accs |> put_accesses name accs' end;
-
-
(* manipulate namings *)
fun reject_qualified name =
@@ -277,6 +297,36 @@
Naming (append path prfx,
(qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
+val apply_prefix =
+ let
+ fun mk_prefix (prfx, true) = sticky_prefix prfx
+ | mk_prefix (prfx, false) = add_path prfx;
+ in fold mk_prefix end;
+
+
+(* declarations *)
+
+fun full (Naming (path, (qualify, _))) = qualify path;
+
+fun declare naming name space =
+ if is_hidden name then
+ error ("Attempt to declare hidden name " ^ quote name)
+ else
+ let
+ val names = explode_name name;
+ val _ = (null names orelse exists (fn s => s = "") names
+ orelse exists_string (fn s => s = "\"") name) andalso
+ error ("Bad name declaration " ^ quote name);
+ val (accs, accs') = pairself (map implode_name) (accesses naming names);
+ in space |> fold (add_name name) accs |> put_accesses name accs' end;
+
+fun declare_binding bnaming (Binding ((prefix, bname), _)) =
+ let
+ val naming = apply_prefix prefix bnaming;
+ val dname = full bnaming bname;
+ val name = full naming bname;
+ in declare naming name #> pair name end;
+
(** name spaces coupled with symbol tables **)
@@ -285,6 +335,17 @@
val empty_table = (empty, Symtab.empty);
+fun gen_table_declare update naming (binding, x) (space, tab) =
+ let
+ val (name, space') = declare_binding naming binding space;
+ in (name, (space', update (name, x) tab)) end;
+
+fun table_declare naming = gen_table_declare Symtab.update_new naming;
+fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
+
+fun full_binding naming (Binding ((prefix, bname), _)) =
+ full (apply_prefix prefix naming) bname;
+
fun extend_table naming bentries (space, tab) =
let val entries = map (apfst (full naming)) bentries
in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
--- a/src/Pure/name.ML Thu Nov 20 10:29:35 2008 +0100
+++ b/src/Pure/name.ML Thu Nov 20 14:51:40 2008 +0100
@@ -28,26 +28,22 @@
val variants: string list -> context -> string list * context
val variant_list: string list -> string list -> string list
val variant: string list -> string -> string
- type binding
- val binding_pos: string * Position.T -> binding
- val binding: string -> binding
- val no_binding: binding
- val prefix_of: binding -> (string * bool) list
- val name_of: binding -> string
- val name_with_prefix: binding -> string (*FIXME*)
- val is_nothing: binding -> bool
- val pos_of: binding -> Position.T
+
+ include NAME_BINDING
val add_prefix: bool -> string -> binding -> binding
val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding
- val map_name: (string -> string) -> binding -> binding
- val qualified: string -> binding -> binding
- val namify: NameSpace.naming -> binding -> NameSpace.naming * string
- val output: binding -> string
+ val name_of: binding -> string (*FIMXE legacy*)
+ val map_name: (string -> string) -> binding -> binding (*FIMXE legacy*)
+ val qualified: string -> binding -> binding (*FIMXE legacy*)
+ val display: binding -> string
+ val namify: NameSpace.naming -> binding -> NameSpace.naming * string (*FIMXE legacy*)
end;
structure Name: NAME =
struct
+open NameSpace;
+
(** common defaults **)
val uu = "uu";
@@ -155,45 +151,37 @@
fun variant used = singleton (variant_list used);
-
(** generic name bindings **)
-datatype binding = Binding of ((string * bool) list * string) * Position.T;
-
-fun prefix_of (Binding ((prefix, _), _)) = prefix;
-fun name_of (Binding ((_, name), _)) = name;
-fun pos_of (Binding (_, pos)) = pos;
-
-fun binding_pos (name, pos) = Binding (([], name), pos);
-fun binding name = binding_pos (name, Position.none);
-val no_binding = binding "";
+fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
+ else (map_binding o apfst) (cons (prfx, sticky)) b;
-fun map_binding f (Binding bnd) = Binding (f bnd);
-
-fun add_prefix sticky prfx binding = if prfx = "" then error "empty name prefix"
- else (map_binding o apfst o apfst) (cons (prfx, sticky)) binding;
-
-fun map_prefix f (Binding ((prefix, name), pos)) =
- f prefix (binding_pos (name, pos));
-
-val map_name = map_binding o apfst o apsnd;
+val prefix_of = fst o dest_binding;
+val name_of = snd o dest_binding;
+val map_name = map_binding o apsnd;
val qualified = map_name o NameSpace.qualified;
-fun is_nothing (Binding ((_, name), _)) = name = "";
+fun map_prefix f b =
+ let
+ val (prefix, name) = dest_binding b;
+ val pos = pos_of b;
+ in f prefix (binding_pos (name, pos)) end;
-fun name_with_prefix (Binding ((prefix, name), _)) =
- NameSpace.implode (map_filter
- (fn (prfx, sticky) => if sticky then SOME prfx else NONE) prefix @ [name]);
-
-fun namify naming (Binding ((prefix, name), _)) =
+fun namify naming b =
let
- fun mk_prefix (prfx, true) = NameSpace.sticky_prefix prfx
- | mk_prefix (prfx, false) = NameSpace.add_path prfx;
+ val (prefix, name) = dest_binding b
+ fun mk_prefix (prfx, true) = sticky_prefix prfx
+ | mk_prefix (prfx, false) = add_path prfx;
val naming' = fold mk_prefix prefix naming;
- in (naming', NameSpace.full naming' name) end;
+ in (naming', full naming' name) end;
-fun output (Binding ((prefix, name), _)) =
- if null prefix orelse name = "" then name
- else NameSpace.implode (map fst prefix) ^ " / " ^ name;
+fun display b =
+ let
+ val (prefix, name) = dest_binding b
+ fun mk_prefix (prfx, true) = prfx
+ | mk_prefix (prfx, false) = enclose "(" ")" prfx
+ in if not (! NameSpace.long_names) orelse null prefix orelse name = "" then name
+ else NameSpace.implode (map mk_prefix prefix) ^ ":" ^ name
+ end;
end;