# HG changeset patch
# User wenzelm
# Date 1427793415 -7200
# Node ID 3ecb48ce92d74138f80eec0f906c02e0c894a696
# Parent  a979fc5db52608628c037aefe8a56f03cfdaecf8
tuned signature;

diff -r a979fc5db526 -r 3ecb48ce92d7 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue Mar 31 00:21:07 2015 +0200
+++ b/src/Pure/General/binding.ML	Tue Mar 31 11:16:55 2015 +0200
@@ -10,7 +10,6 @@
 signature BINDING =
 sig
   eqtype binding
-  val dest: binding -> {private: bool, concealed: bool, path: (string * bool) list, name: bstring}
   val path_of: binding -> (string * bool) list
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
@@ -36,6 +35,8 @@
   val pp: binding -> Pretty.T
   val bad: binding -> string
   val check: binding -> unit
+  val name_spec: (string * bool) list -> binding ->
+    {private: bool, concealed: bool, spec: (string * bool) list}
 end;
 
 structure Binding: BINDING =
@@ -46,7 +47,7 @@
 (* datatype *)
 
 datatype binding = Binding of
- {private: bool,                    (*entry is strictly private -- no name space accesses*)
+ {private: bool,                    (*entry is private -- no name space accesses, only full name*)
   concealed: bool,                  (*entry is for foundational purposes -- please ignore*)
   prefix: (string * bool) list,     (*system prefix*)
   qualifier: (string * bool) list,  (*user qualifier*)
@@ -60,10 +61,7 @@
 fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
   make_binding (f (private, concealed, prefix, qualifier, name, pos));
 
-fun dest (Binding {private, concealed, prefix, qualifier, name, ...}) =
-  {private = private, concealed = concealed, path = prefix @ qualifier, name = name};
-
-val path_of = #path o dest;
+fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
 
 
 
@@ -157,6 +155,26 @@
   if Symbol_Pos.is_identifier (name_of binding) then ()
   else legacy_feature (bad binding);
 
+
+
+(** resulting name_spec **)
+
+val bad_specs = ["", "??", "__"];
+
+fun name_spec path binding =
+  let
+    val Binding {private, concealed, prefix, qualifier, name, ...} = binding;
+    val _ = Long_Name.is_qualified name andalso error (bad binding);
+
+    val spec1 =
+      maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
+    val spec2 = if name = "" then [] else [(name, true)];
+    val spec = spec1 @ spec2;
+    val _ =
+      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
+      andalso error (bad binding);
+  in {private = private, concealed = concealed, spec = if null spec2 then [] else spec} end;
+
 end;
 
 type binding = Binding.binding;
diff -r a979fc5db526 -r 3ecb48ce92d7 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 31 00:21:07 2015 +0200
+++ b/src/Pure/General/name_space.ML	Tue Mar 31 11:16:55 2015 +0200
@@ -319,6 +319,8 @@
 fun new_group naming = set_group (SOME (serial ())) naming;
 val reset_group = set_group NONE;
 
+fun get_path (Naming {path, ...}) = path;
+
 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
 val root_path = map_path (fn _ => []);
 val parent_path = map_path (perhaps (try (#1 o split_last)));
@@ -333,27 +335,12 @@
 
 (* full name *)
 
-fun err_bad binding = error (Binding.bad binding);
-
 fun transform_binding (Naming {private, concealed, ...}) =
   private ? Binding.private #>
   concealed ? Binding.concealed;
 
-val bad_specs = ["", "??", "__"];
-
-fun name_spec (naming as Naming {path = path1, ...}) raw_binding =
-  let
-    val binding = transform_binding naming raw_binding;
-    val {private, concealed, path = path2, name} = Binding.dest binding;
-    val _ = Long_Name.is_qualified name andalso err_bad binding;
-
-    val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path1 @ path2);
-    val spec2 = if name = "" then [] else [(name, true)];
-    val spec = spec1 @ spec2;
-    val _ =
-      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
-      andalso err_bad binding;
-  in {private = private, concealed = concealed, spec = if null spec2 then [] else spec} end;
+fun name_spec naming binding =
+  Binding.name_spec (get_path naming) (transform_binding naming binding);
 
 fun full_name naming =
   name_spec naming #> #spec #> map #1 #> Long_Name.implode;
@@ -446,7 +433,7 @@
     val (accs, accs') = accesses naming binding;
 
     val name = Long_Name.implode (map fst spec);
-    val _ = name = "" andalso err_bad binding;
+    val _ = name = "" andalso error (Binding.bad binding);
 
     val (proper_pos, pos) = Position.default (Binding.pos_of binding);
     val entry =