From 86af949158e013178557c7fec7662ac06fae753c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 26 Sep 2005 16:27:58 +0000 Subject: [PATCH] if a node has an xref use it for cut and paste, no matter if it have an href as well --- helm/matita/matitaMathView.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 6074fdae7..4297634c8 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -272,9 +272,9 @@ object (self) (try Hashtbl.find ids_to_terms id with Not_found -> assert false) method private string_of_node node = - if node#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href_ds - then string_of_dom_node node - else self#string_of_id_node node + if node#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds + then self#string_of_id_node node + else string_of_dom_node node method private string_of_id_node node = let get_id (node: Gdome.element) = -- 2.39.2