1.1 --- a/src/Pure/General/binding.ML	Thu Mar 05 10:19:51 2009 +0100
     1.2 +++ b/src/Pure/General/binding.ML	Thu Mar 05 10:52:07 2009 +0100
     1.3 @@ -10,17 +10,18 @@
     1.4  signature BINDING =
     1.5  sig
     1.6    type binding
     1.7 -  val dest: binding -> (string * bool) list * (string * bool) list * bstring
     1.8 +  val dest: binding -> (string * bool) list * bstring
     1.9    val verbose: bool ref
    1.10    val str_of: binding -> string
    1.11    val make: bstring * Position.T -> binding
    1.12 +  val pos_of: binding -> Position.T
    1.13    val name: bstring -> binding
    1.14 -  val pos_of: binding -> Position.T
    1.15    val name_of: binding -> string
    1.16    val map_name: (bstring -> bstring) -> binding -> binding
    1.17    val empty: binding
    1.18    val is_empty: binding -> bool
    1.19    val qualify: bool -> string -> binding -> binding
    1.20 +  val prefix_of: binding -> (string * bool) list
    1.21    val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
    1.22    val add_prefix: bool -> string -> binding -> binding
    1.23  end;
    1.24 @@ -32,13 +33,11 @@
    1.25  
    1.26  (* datatype *)
    1.27  
    1.28 -type component = string * bool;   (*name with mandatory flag*)
    1.29 -
    1.30  datatype binding = Binding of
    1.31 - {prefix: component list,         (*system prefix*)
    1.32 -  qualifier: component list,      (*user qualifier*)
    1.33 -  name: bstring,                  (*base name*)
    1.34 -  pos: Position.T};               (*source position*)
    1.35 + {prefix: (string * bool) list,     (*system prefix*)
    1.36 +  qualifier: (string * bool) list,  (*user qualifier*)
    1.37 +  name: bstring,                    (*base name*)
    1.38 +  pos: Position.T};                 (*source position*)
    1.39  
    1.40  fun make_binding (prefix, qualifier, name, pos) =
    1.41    Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
    1.42 @@ -46,7 +45,7 @@
    1.43  fun map_binding f (Binding {prefix, qualifier, name, pos}) =
    1.44    make_binding (f (prefix, qualifier, name, pos));
    1.45  
    1.46 -fun dest (Binding {prefix, qualifier, name, ...}) = (prefix, qualifier, name);
    1.47 +fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name);
    1.48  
    1.49  
    1.50  (* diagnostic output *)
    1.51 @@ -92,6 +91,8 @@
    1.52  
    1.53  (* system prefix *)
    1.54  
    1.55 +fun prefix_of (Binding {prefix, ...}) = prefix;
    1.56 +
    1.57  fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
    1.58    (f prefix, qualifier, name, pos));
    1.59