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