# HG changeset patch
# User wenzelm
# Date 1236246727 -3600
# Node ID 51b92d34af792e846446775226126742f170da5b
# Parent  381ce8d88cb83fde2c26ab54a514b6fa054fb0f2
added prefix_of;
tuned signature;
tuned;

diff -r 381ce8d88cb8 -r 51b92d34af79 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Thu Mar 05 10:19:51 2009 +0100
+++ b/src/Pure/General/binding.ML	Thu Mar 05 10:52:07 2009 +0100
@@ -10,17 +10,18 @@
 signature BINDING =
 sig
   type binding
-  val dest: binding -> (string * bool) list * (string * bool) list * bstring
+  val dest: binding -> (string * bool) list * bstring
   val verbose: bool ref
   val str_of: binding -> string
   val make: bstring * Position.T -> binding
+  val pos_of: binding -> Position.T
   val name: bstring -> binding
-  val pos_of: binding -> Position.T
   val name_of: binding -> string
   val map_name: (bstring -> bstring) -> binding -> binding
   val empty: binding
   val is_empty: binding -> bool
   val qualify: bool -> string -> binding -> binding
+  val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val add_prefix: bool -> string -> binding -> binding
 end;
@@ -32,13 +33,11 @@
 
 (* datatype *)
 
-type component = string * bool;   (*name with mandatory flag*)
-
 datatype binding = Binding of
- {prefix: component list,         (*system prefix*)
-  qualifier: component list,      (*user qualifier*)
-  name: bstring,                  (*base name*)
-  pos: Position.T};               (*source position*)
+ {prefix: (string * bool) list,     (*system prefix*)
+  qualifier: (string * bool) list,  (*user qualifier*)
+  name: bstring,                    (*base name*)
+  pos: Position.T};                 (*source position*)
 
 fun make_binding (prefix, qualifier, name, pos) =
   Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
@@ -46,7 +45,7 @@
 fun map_binding f (Binding {prefix, qualifier, name, pos}) =
   make_binding (f (prefix, qualifier, name, pos));
 
-fun dest (Binding {prefix, qualifier, name, ...}) = (prefix, qualifier, name);
+fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name);
 
 
 (* diagnostic output *)
@@ -92,6 +91,8 @@
 
 (* system prefix *)
 
+fun prefix_of (Binding {prefix, ...}) = prefix;
+
 fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
   (f prefix, qualifier, name, pos));