enable selections and href handling on elements having href and no xref, this

permits selecting/following links on case pattern heads and outtype

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index b2708fe298b86cd71627c9da7afae88a8be5ead3..47f8c5a5c13d33320deb010b7a81df0187d6d285 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -105,6 +105,17 @@ let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types =
   | Cic.AInductiveDefinition _ ->
       assert false  (* TODO *)
 
+  (** @return string content of a dom node having a single text child node, e.g.
+   * <m:mi xlink:href="...">bool</m:mi> *)
+let string_of_dom_node node =
+  match node#get_firstChild with
+  | None -> ""
+  | Some node ->
+      (try
+        let text = new Gdome.text_of_node node in
+        text#get_data#to_string
+      with GdomeInit.DOMCastException _ -> "")
+
 class clickableMathView obj =
 let text_width = 80 in
 object (self)
@@ -211,18 +222,18 @@ object (self)
   method private choose_selection_cb gdome_elt =
     let (gui: MatitaGuiTypes.gui) = get_gui () in
     let clipboard = GData.clipboard Gdk.Atom.primary in
+    let set_selection elt =
+      self#set_selection (Some elt);
+      self#coerce#misc#add_selection_target
+        ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary;
+      ignore (self#coerce#misc#grab_selection Gdk.Atom.primary)
+    in
     let rec aux elt =
       if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
             ~localName:xref_ds)#to_string <> ""
-(*         if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
-        && (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
-            ~localName:xref_ds)#to_string <> "" *)
-      then begin
-        self#set_selection (Some elt);
-        self#coerce#misc#add_selection_target
-          ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary;
-        ignore (self#coerce#misc#grab_selection Gdk.Atom.primary)
-      end else
+      then
+        set_selection elt
+      else
         try
           (match elt#get_parentNode with
           | None -> assert false
@@ -230,6 +241,9 @@ object (self)
         with GdomeInit.DOMCastException _ -> ()
     in
     (match gdome_elt with
+    | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns
+        ~localName:href_ds)#to_string <> "" ->
+          set_selection elt
     | Some elt -> aux elt
     | None -> self#set_selection None);
     selection_changed <- true
@@ -258,6 +272,11 @@ 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
+
+  method private string_of_id_node node =
     let get_id (node: Gdome.element) =
       let xref_attr =
         node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds