- let make_href xmlattrs xref uris =
- let xref_uri = lookup_uri !xref in
- let raw_uris = List.map UriManager.string_of_uri !uris in
- let uri =
- match xref_uri, raw_uris with
- | None, [] -> None
- | Some uri, [] -> Some uri
- | None, raw_uris -> Some (String.concat " " raw_uris)
- | Some uri, raw_uris -> Some (String.concat " " (uri :: raw_uris))
+ let make_href xmlattrs xref =
+ let xref_uris =
+ List.fold_right
+ (fun xref uris ->
+ match lookup_uri xref with
+ | None -> uris
+ | Some uri -> uri :: uris)
+ !xref []
+ in
+ let xmlattrs_uris, xmlattrs =
+ let xref_attrs, other_attrs =
+ List.partition
+ (function Some "xlink", "href", _ -> true | _ -> false)
+ xmlattrs
+ in
+ List.map (fun (_, _, uri) -> uri) xref_attrs,
+ other_attrs
+ in
+ let uris =
+ match xmlattrs_uris @ xref_uris with
+ | [] -> None
+ | uris ->
+ Some (String.concat " "
+ (HExtlib.list_uniq (List.sort String.compare uris)))
+ in
+ let xrefs =
+ match !xref with [] -> None | xrefs -> Some (String.concat " " xrefs)