# HG changeset patch # User wenzelm # Date 1236528187 -3600 # Node ID 8ea7a197e2e6415f13dc95343ed1266bee7139a1 # Parent d4d3fafc9bcaf0f3703767f45fbe48deae8ca0f4 added qualified_name -- emulates old-style qualified bstring; tuned; diff -r d4d3fafc9bca -r 8ea7a197e2e6 src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Sun Mar 08 16:53:38 2009 +0100 +++ b/src/Pure/General/binding.ML Sun Mar 08 17:03:07 2009 +0100 @@ -22,6 +22,7 @@ val eq_name: binding * binding -> bool val empty: binding val is_empty: binding -> bool + val qualified_name: bstring -> binding val qualify: bool -> string -> binding -> binding val prefix_of: binding -> (string * bool) list val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding @@ -51,7 +52,7 @@ fun str_of (Binding {prefix, qualifier, name, pos}) = let - val text = space_implode "." (map #1 qualifier @ [name]); + val text = Long_Name.implode (map #1 qualifier @ [name]); val props = Position.properties_of pos; in Markup.markup (Markup.properties props (Markup.binding name)) text end; @@ -79,6 +80,11 @@ (* user qualifier *) +fun qualified_name "" = empty + | qualified_name s = + let val (qualifier, name) = split_last (Long_Name.explode s) + in make_binding ([], map (rpair false) qualifier, name, Position.none) end; + fun qualify _ "" = I | qualify strict qual = map_binding (fn (prefix, qualifier, name, pos) => (prefix, (qual, strict) :: qualifier, name, pos));