# HG changeset patch
# User haftmann
# Date 1227189100 -3600
# Node ID b1d46059d502ec1f20fe76d5ee1b8230dcd5c056
# Parent  d50b523c55db2f12272f4873d78c915243e2bdba
name spaces and name bindings

diff -r d50b523c55db -r b1d46059d502 src/Pure/General/name_space.ML
--- 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;
diff -r d50b523c55db -r b1d46059d502 src/Pure/name.ML
--- 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;