# HG changeset patch # User wenzelm # Date 1236101519 -3600 # Node ID 4102bbf2af21357cfbe07d132b7ea4b942894b76 # Parent 14145e81a2fef89fc76df78f40eafc2d962858f1 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings; moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names; type binding: maintain explicit qualifier, indepently of base name; tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused); Binding.str_of: include markup with position properties; misc tuning; diff -r 14145e81a2fe -r 4102bbf2af21 src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Tue Mar 03 17:42:30 2009 +0100 +++ b/src/Pure/General/binding.ML Tue Mar 03 18:31:59 2009 +0100 @@ -5,77 +5,93 @@ Structured name bindings. *) +type bstring = string; (*primitive names to be bound*) + signature BINDING = sig - val separator: string - val is_qualified: string -> bool type binding + val dest: binding -> (string * bool) list * (string * bool) list * bstring val str_of: binding -> string - val name_pos: string * Position.T -> binding - val name: string -> binding + val make: bstring * Position.T -> binding + 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 map_base: (string -> string) -> binding -> binding - val qualify: string -> binding -> binding + val is_empty: binding -> bool + val qualify: bool -> string -> binding -> binding + val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding val add_prefix: bool -> string -> binding -> binding - val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding - val is_empty: binding -> bool - val base_name: binding -> string - val pos_of: binding -> Position.T - val dest: binding -> (string * bool) list * string end; structure Binding: BINDING = struct -(** qualification **) - -val separator = "."; -val is_qualified = exists_string (fn s => s = separator); +(** representation **) -fun reject_qualified kind s = - if is_qualified s then - error ("Attempt to declare qualified " ^ kind ^ " " ^ quote s) - else s; +(* datatype *) +type component = string * bool; (*name with mandatory flag*) -(** binding representation **) - -datatype binding = Binding of ((string * bool) list * string) * Position.T; - (* (prefix components (with mandatory flag), base name, position) *) +datatype binding = Binding of + {prefix: component list, (*system prefix*) + qualifier: component list, (*user qualifier*) + name: bstring, (*base name*) + pos: Position.T}; (*source position*) -fun str_of (Binding ((prefix, name), _)) = - let - fun mk_prefix (prfx, true) = prfx - | mk_prefix (prfx, false) = enclose "(" ")" prfx - in space_implode "." (map mk_prefix prefix) ^ ":" ^ name end; +fun make_binding (prefix, qualifier, name, pos) = + Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos}; + +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 name_pos (name, pos) = Binding (([], name), pos); -fun name name = name_pos (name, Position.none); -val empty = name ""; +(* diagnostic output *) -fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos); +val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?"); -val map_base = map_binding o apsnd; +fun str_of (Binding {prefix, qualifier, name, pos}) = + let + val text = + (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^ + str_of_components qualifier ^ ":" ^ name; + val props = Position.properties_of pos; + in Markup.markup (Markup.properties props (Markup.binding name)) text end; -fun qualify_base path name = - if path = "" orelse name = "" then name - else path ^ separator ^ name; + + +(** basic operations **) + +(* name and position *) + +fun make (name, pos) = make_binding ([], [], name, pos); +fun name name = make (name, Position.none); -val qualify = map_base o qualify_base; - (*FIXME should all operations on bare names move here from name_space.ML ?*) +fun pos_of (Binding {pos, ...}) = pos; +fun name_of (Binding {name, ...}) = name; + +fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos)); -fun add_prefix sticky "" b = b - | add_prefix sticky prfx b = (map_binding o apfst) - (cons ((*reject_qualified "prefix"*) prfx, sticky)) b; +val empty = name ""; +fun is_empty b = name_of b = ""; + + +(* user qualifier *) -fun map_prefix f (Binding ((prefix, name), pos)) = - f prefix (name_pos (name, pos)); +fun qualify _ "" = I + | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) => + (prefix, (qual, mandatory) :: qualifier, name, pos)); + -fun is_empty (Binding ((_, name), _)) = name = ""; -fun base_name (Binding ((_, name), _)) = name; -fun pos_of (Binding (_, pos)) = pos; -fun dest (Binding (prefix_name, _)) = prefix_name; +(* system prefix *) + +fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) => + (f prefix, qualifier, name, pos)); + +fun add_prefix _ "" = I + | add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory)); end; diff -r 14145e81a2fe -r 4102bbf2af21 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Tue Mar 03 17:42:30 2009 +0100 +++ b/src/Pure/General/name_space.ML Tue Mar 03 18:31:59 2009 +0100 @@ -6,7 +6,6 @@ Cf. Pure/General/binding.ML *) -type bstring = string; (*simple names to be bound -- legacy*) type xstring = string; (*external names*) signature BASIC_NAME_SPACE = @@ -67,8 +66,8 @@ fun hidden name = "??." ^ name; val is_hidden = String.isPrefix "??."; -val separator = Binding.separator; -val is_qualified = Binding.is_qualified; +val separator = "."; +val is_qualified = exists_string (fn s => s = separator); val implode_name = space_implode separator; val explode_name = space_explode separator; @@ -295,13 +294,13 @@ in space |> fold (add_name name) accs |> put_accesses name accs' end; fun full_name naming b = - let val (prefix, bname) = Binding.dest b - in full_internal (apply_prefix prefix naming) bname end; + let val (prefix, qualifier, bname) = Binding.dest b + in full_internal (apply_prefix (prefix @ qualifier) naming) bname end; fun declare bnaming b = let - val (prefix, bname) = Binding.dest b; - val naming = apply_prefix prefix bnaming; + val (prefix, qualifier, bname) = Binding.dest b; + val naming = apply_prefix (prefix @ qualifier) bnaming; val name = full_internal naming bname; in declare_internal naming name #> pair name end;