From: Stefano Zacchiroli Date: Mon, 26 Sep 2005 16:27:58 +0000 (+0000) Subject: if a node has an xref use it for cut and paste, no matter if it have an href as well X-Git-Tag: V_0_7_2_3~308 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=86af949158e013178557c7fec7662ac06fae753c;p=helm.git if a node has an xref use it for cut and paste, no matter if it have an href as well --- 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) =