]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaMathView.ml
snapshot, notably:
[helm.git] / helm / matita / matitaMathView.ml
index d485ac02588c66e31510ed7a6d6fed2935122bb6..f264ec413cad9c51932a3c804d3c88fe3ca60c9c 100644 (file)
@@ -44,114 +44,122 @@ let list_map_fail f =
  in
   aux
 
-let choose_selection mmlwidget (element : Gdome.element option) =
-  let rec aux element =
-    if element#hasAttributeNS
-       ~namespaceURI:Misc.helmns
-       ~localName:(Gdome.domString "xref")
-    then
-      mmlwidget#set_selection (Some element)
-    else
-      try
-        match element#get_parentNode with
-        | None -> assert false
-        | Some p -> aux (new Gdome.element_of_node p)
-      with GdomeInit.DOMCastException _ ->
-        debug_print "trying to select above the document root"
-  in
-  match element with
-  | Some x -> aux x
-  | None   -> mmlwidget#set_selection None
+class clickable_math_view obj =
+  let href = Gdome.domString "href" in
+  let xref = Gdome.domString "xref" in
+  object (self)
+    inherit GMathViewAux.multi_selection_math_view obj
+
+    val mutable href_callback: (UriManager.uri -> unit) option = None
+    method set_href_callback f = href_callback <- f
+
+    initializer
+      ignore (self#connect#selection_changed self#choose_selection);
+      ignore (self#connect#click (fun (gdome_elt, _, _, _) ->
+        match gdome_elt with
+        | Some elt  (* element is an hyperlink, use href_callback on it *)
+          when elt#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href ->
+            (match href_callback with
+            | None -> ()
+            | Some f ->
+                let uri =
+                  elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href
+                in
+                f (UriManager.uri_of_string (uri#to_string)))
+        | Some elt -> ignore (self#action_toggle elt)
+        | None -> ()))
+    method private choose_selection gdome_elt =
+      let rec aux elt =
+        if elt#hasAttributeNS ~namespaceURI:Misc.helm_ns ~localName:xref then
+          self#set_selection (Some elt)
+        else
+          try
+            (match elt#get_parentNode with
+            | None -> assert false
+            | Some p -> aux (new Gdome.element_of_node p))
+          with GdomeInit.DOMCastException _ -> ()
+(*             debug_print "trying to select above the document root" *)
+      in
+      match gdome_elt with
+      | Some elt -> aux elt
+      | None   -> self#set_selection None
+  end
 
 class proof_viewer obj =
- object(self)
 object(self)
 
-  inherit GMathViewAux.single_selection_math_view obj
+    inherit clickable_math_view obj
 
-  val mutable current_infos = None
-  val mutable current_mathml = None
+    val mutable current_infos = None
+    val mutable current_mathml = None
 
-  initializer
-    ignore (self#connect#click (fun (gdome_elt, _, _, _) ->
-      match gdome_elt with
-      | Some gdome_elt ->
-          prerr_endline (gdome_elt#get_nodeName#to_string);
-          ignore (self#action_toggle gdome_elt)
-      | None -> ()));
-    ignore (self#connect#selection_changed (choose_selection self))
-
-  method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
-    let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
-        ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
-      Cic2acic.acic_object_of_cic_object (cicCurrentProof proof)
-    in
-    current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_conjectures,
-      ids_to_hypotheses);
-    let mathml =
-      ApplyTransformation.mml_of_cic_object ~explode_all:true
-        (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types
-    in
-    debug_print "load_proof: dumping MathML to ./proof";
-    ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
-    match current_mathml with
-    |  None ->
-        self#load_root ~root:mathml#get_documentElement ;
-        current_mathml <- Some mathml
-    | Some current_mathml ->
-        self#freeze;
-        XmlDiff.update_dom ~from:current_mathml mathml ;
-        self#thaw
+    method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
+      let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
+          ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
+        Cic2acic.acic_object_of_cic_object (cicCurrentProof proof)
+      in
+      current_infos <- Some (ids_to_terms, ids_to_father_ids,
+        ids_to_conjectures, ids_to_hypotheses);
+      let mathml =
+        ApplyTransformation.mml_of_cic_object ~explode_all:true
+          (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types
+      in
+      debug_print "load_proof: dumping MathML to ./proof";
+      ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
+      match current_mathml with
+      |  None ->
+          self#load_root ~root:mathml#get_documentElement ;
+          current_mathml <- Some mathml
+      | Some current_mathml ->
+          self#freeze;
+          XmlDiff.update_dom ~from:current_mathml mathml ;
+          self#thaw
   end
 
 class sequent_viewer obj =
- object(self)
-
-  inherit GMathViewAux.multi_selection_math_view obj
+  object(self)
 
-  initializer
-    ignore (self#connect#selection_changed (choose_selection self))
+    inherit clickable_math_view obj
 
-  val mutable current_infos = None
+    val mutable current_infos = None
 
-  method get_selected_terms =
-   let selections = self#get_selections in
-    list_map_fail
-     (function node ->
-       let xpath =
-        ((node : Gdome.element)#getAttributeNS
-          ~namespaceURI:Misc.helmns
-          ~localName:(Gdome.domString "xref"))#to_string
-       in
-        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
-        else
-         match current_infos with
-            Some (ids_to_terms,_,_) ->
-             let id = xpath in
-              (try
-                Hashtbl.find ids_to_terms id
-               with _ -> raise Skip)
-          | None -> assert false (* "ERROR: No current term!!!" *)
-     ) selections
-
-  method get_selected_hypotheses =
-   let selections = self#get_selections in
-    list_map_fail
-     (function node ->
-       let xpath =
-        ((node : Gdome.element)#getAttributeNS
-          ~namespaceURI:Misc.helmns
-          ~localName:(Gdome.domString "xref"))#to_string
-       in
-        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
-        else
-         match current_infos with
-            Some (_,_,ids_to_hypotheses) ->
-             let id = xpath in
-              (try
-                Hashtbl.find ids_to_hypotheses id
-               with _ -> raise Skip)
-          | None -> assert false (* "ERROR: No current term!!!" *)
-     ) selections
+    method get_selected_terms =
+      let selections = self#get_selections in
+      list_map_fail
+        (fun node ->
+          let xpath =
+            ((node : Gdome.element)#getAttributeNS
+              ~namespaceURI:Misc.helm_ns
+              ~localName:(Gdome.domString "xref"))#to_string
+          in
+          if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+          else
+            match current_infos with
+            | Some (ids_to_terms,_,_) ->
+                (try
+                  Hashtbl.find ids_to_terms xpath
+                 with _ -> raise Skip)
+            | None -> assert false) (* "ERROR: No current term!!!" *)
+        selections
+
+    method get_selected_hypotheses =
+      let selections = self#get_selections in
+      list_map_fail
+        (fun node ->
+          let xpath =
+            ((node : Gdome.element)#getAttributeNS
+              ~namespaceURI:Misc.helm_ns
+              ~localName:(Gdome.domString "xref"))#to_string
+          in
+          if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+          else
+            match current_infos with
+            | Some (_,_,ids_to_hypotheses) ->
+                (try
+                  Hashtbl.find ids_to_hypotheses xpath
+                with _ -> raise Skip)
+            | None -> assert false) (* "ERROR: No current term!!!" *)
+        selections
   
   method load_sequent metasenv metano =
 (*
@@ -281,13 +289,20 @@ let sequents_viewer ~(notebook:GPack.notebook)
 =
   new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
 
-let check_widget =
-  lazy
-    (let gui = MatitaGui.instance () in
-    sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add ())
-
 class mathViewer =
+  let href_callback: (UriManager.uri -> unit) option ref = ref None in
   object
+    val check_widget =
+      lazy
+        (let gui = MatitaGui.instance () in
+        let sequent_viewer =
+          sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add ()
+        in
+        sequent_viewer#set_href_callback !href_callback;
+        sequent_viewer)
+
+    method set_href_callback f = href_callback := f
+
     method checkTerm sequent metasenv =
       let (metano, context, expr) = sequent in
       let widget = Lazy.force check_widget in