X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaMathView.ml;h=ee18823f5ba617953af6f971e8c5f21529bb8381;hb=cec61c8b027b15b98d308cee8900d9cf35a02d28;hp=f9171068f2158d07ca7dcc1695ed7a638a57d5d6;hpb=789bd6e2f5d8678421c6043359be50b695720d3f;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index f9171068f..ee18823f5 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -66,6 +66,13 @@ let increase_font_size () = incr current_font_size
 let decrease_font_size () = decr current_font_size
 let reset_font_size () = current_font_size := default_font_size ()
 
+  (* is there any lablgtk2 constant corresponding to the left mouse button??? *)
+let left_button = 1
+
+let near (x1, y1) (x2, y2) =
+  let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
+  (distance < 4.)
+
 class clickableMathView obj =
   let href = Gdome.domString "href" in
   let xref = Gdome.domString "xref" in
@@ -78,9 +85,11 @@ class clickableMathView obj =
     initializer
       self#set_font_size !current_font_size;
       ignore (self#connect#selection_changed self#choose_selection);
-      ignore (self#connect#click (fun (gdome_elt, _, _, _) ->
+      ignore (self#event#connect#button_press self#button_press);
+      ignore (self#event#connect#button_release self#button_release);
+(*       ignore (self#connect#click (fun (gdome_elt, _, _, _) ->
         match gdome_elt with
-        | Some elt  (* element is an hyperlink, use href_callback on it *)
+        | Some elt  |+ element is an hyperlink, use href_callback on it +|
           when elt#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href ->
             (match href_callback with
             | None -> ()
@@ -90,7 +99,57 @@ class clickableMathView obj =
                 in
                 f (uri#to_string))
         | Some elt -> ignore (self#action_toggle elt)
-        | None -> ()))
+        | None -> ())) *)
+
+    val mutable button_press_x = -1.
+    val mutable button_press_y = -1.
+
+    method private button_press gdk_button =
+      button_press_x <- GdkEvent.Button.x gdk_button;
+      button_press_y <- GdkEvent.Button.y gdk_button;
+      false
+
+    method private button_release gdk_button =
+      let button_release_x = GdkEvent.Button.x gdk_button in
+      let button_release_y = GdkEvent.Button.y gdk_button in
+      (if near (button_press_x, button_press_y)
+        (button_release_x, button_release_y)
+      then
+        let x = int_of_float button_press_x in
+        let y = int_of_float button_press_y in
+        (match self#get_element_at x y with
+        | None -> ()
+        | Some elt ->
+            let namespaceURI = DomMisc.xlink_ns in
+            let localName = href in
+            if elt#hasAttributeNS ~namespaceURI ~localName then
+              self#invoke_href_callback
+                (elt#getAttributeNS ~namespaceURI ~localName)#to_string
+                gdk_button
+            else
+              ignore (self#action_toggle elt)));
+      false
+
+    method private invoke_href_callback href_value gdk_button =
+      let button = GdkEvent.Button.button gdk_button in
+      if button = left_button then
+        let time = GdkEvent.Button.time gdk_button in
+        match href_callback with
+        | None -> ()
+        | Some f ->
+            (match MatitaMisc.split href_value with
+            | [ uri ] ->  f uri
+            | uris ->
+                let menu = GMenu.menu () in
+                List.iter
+                  (fun uri ->
+                    let menu_item =
+                      GMenu.menu_item ~label:uri ~packing:menu#append ()
+                    in
+                    ignore (menu_item#connect#activate (fun () -> f uri)))
+                  uris;
+                menu#popup ~button ~time)
+
     method private choose_selection gdome_elt =
       let rec aux elt =
         if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref then
@@ -167,10 +226,9 @@ class sequentViewer obj =
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
     current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
-(*
-    debug_print "load_sequent: dumping MathML to ./prova";
-    ignore (DomMisc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
-*)
+    let name = "sequent_viewer.xml" in
+    prerr_endline ("load_sequent: dumping MathML to ./" ^ name);
+    ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
  end
 
@@ -219,6 +277,7 @@ class sequentsViewer ~(notebook:GPack.notebook)
       _metasenv <- metasenv;
       pages <- sequents_no;
       self#script#setGoal goal;
+      let parentref = ref None in
       let win metano =
         let w =
           GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
@@ -227,8 +286,13 @@ class sequentsViewer ~(notebook:GPack.notebook)
         let reparent () =
           scrolledWin <- Some w;
           match sequentViewer#misc#parent with
-          | None -> w#add sequentViewer#coerce
-          | Some _ -> sequentViewer#misc#reparent w#coerce
+          | None -> w#add sequentViewer#coerce; parentref := Some w
+          | Some parent ->
+             let parent =
+              match !parentref with None -> assert false | Some p -> p in
+             parent#remove sequentViewer#coerce;
+             w#add sequentViewer#coerce;
+             parentref := Some w;
         in
         goal2win <- (metano, reparent) :: goal2win;
         w#coerce
@@ -556,6 +620,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           XmlDiff.update_dom ~from:current_mathml mathml;
           mathView#thaw
       |  _ ->
+          let name = "cic_browser.xml" in
+          prerr_endline ("cic_browser: dumping MathML to ./" ^ name);
+          ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
           mathView#load_root ~root:mathml#get_documentElement;
           current_mathml <- Some mathml);