# HG changeset patch
# User haftmann
# Date 1226937626 -3600
# Node ID 78a6ed46ad04d98ea46b3deb1da26d911a9ee98e
# Parent  95dd21624c6ccb443f9011c9e14c7328ef275420
Name.name_with_prefix (temporarily)

diff -r 95dd21624c6c -r 78a6ed46ad04 src/Pure/name.ML
--- a/src/Pure/name.ML	Mon Nov 17 17:00:22 2008 +0100
+++ b/src/Pure/name.ML	Mon Nov 17 17:00:26 2008 +0100
@@ -34,9 +34,11 @@
   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
   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
@@ -168,14 +170,21 @@
 
 fun map_binding f (Binding bnd) = Binding (f bnd);
 
-fun add_prefix sticky prfx = (map_binding o apfst o apfst)
-  (cons (prfx, sticky));
+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 qualified = map_name o NameSpace.qualified;
 
 fun is_nothing (Binding ((_, name), _)) = name = "";
 
+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), _)) =
   let
     fun mk_prefix (prfx, true) = NameSpace.sticky_prefix prfx