X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=f57dc4d320824cd2e67fb213a5368c5dd596c16a;hb=275b124e484510dc49141f86b5174f8bd0be7d97;hp=70079c4726a0729527cebbfb2974d774edb2c81d;hpb=7a060397679753a0233139b1ba83ac83c2c49949;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 70079c472..f57dc4d32 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -65,9 +65,11 @@ let near (x1, y1) (x2, y2) =
   let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
   (distance < 4.)
 
+let mathml_ns = Gdome.domString "http://www.w3.org/1998/Math/MathML"
 let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink"
 let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm"
 let href_ds = Gdome.domString "href"
+let maction_ds = Gdome.domString "maction"
 let xref_ds = Gdome.domString "xref"
 
 let domImpl = Gdome.domImplementation ()
@@ -163,6 +165,18 @@ let hrefs_of_elt elt =
   else
     None
 
+let rec has_maction (elt :Gdome.element) = 
+  (* fix this comparison *)
+  if elt#get_tagName#to_string = "m:maction" ||
+   elt#get_tagName#to_string = "b:action" then
+    true
+  else 
+    match elt#get_parentNode with
+    | Some node when node#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE -> 
+        has_maction (new Gdome.element_of_node node)
+    | _ -> false
+;;
+
 class clickableMathView obj =
 let text_width = 80 in
 object (self)
@@ -176,7 +190,8 @@ object (self)
   method private cic_info = _cic_info
 
   val normal_cursor = Gdk.Cursor.create `LEFT_PTR
-  val href_cursor = Gdk.Cursor.create `HAND1
+  val href_cursor = Gdk.Cursor.create `HAND2
+  val maction_cursor = Gdk.Cursor.create `QUESTION_ARROW
 
   initializer
     self#set_font_size !current_font_size;
@@ -221,7 +236,11 @@ object (self)
       button_press_y <- GdkEvent.Button.y gdk_button;
       selection_changed <- false
     end else if button = right_button then
-      self#popup_contextual_menu (GdkEvent.Button.time gdk_button);
+      self#popup_contextual_menu 
+        (self#get_element_at 
+          (int_of_float (GdkEvent.Button.x gdk_button)) 
+          (int_of_float (GdkEvent.Button.y gdk_button)))  
+        (GdkEvent.Button.time gdk_button);
     false
 
   method private element_over_cb (elt_opt, _, _, _) =
@@ -233,6 +252,9 @@ object (self)
     in
     match elt_opt with
     | Some elt ->
+        if has_maction elt then
+          Gdk.Window.set_cursor (win ()) maction_cursor
+        else
         (match hrefs_of_elt elt with
         | Some ((_ :: _) as hrefs) ->
             Gdk.Window.set_cursor (win ()) href_cursor;
@@ -274,22 +296,36 @@ object (self)
     | [] -> assert false (* this method is invoked only if there's a sel. *)
     | node :: _ -> self#tactic_text_pattern_of_node node
 
-  method private popup_contextual_menu time =
+  method private popup_contextual_menu element time =
     let menu = GMenu.menu () in
     let add_menu_item ?(menu = menu) ?stock ?label () =
       GMenu.image_menu_item ?stock ?label ~packing:menu#append () in
     let check = add_menu_item ~label:"Check" () in
     let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in
     let tactics_menu_item = GMenu.menu_item ~label:"Apply tactic" () in
+    let hyperlinks_menu_item = GMenu.menu_item ~label:"Hyperlinks" () in
     menu#append reductions_menu_item;
     menu#append tactics_menu_item;
+    menu#append hyperlinks_menu_item;
     let reductions = GMenu.menu () in
     let tactics = GMenu.menu () in
+    let hyperlinks = GMenu.menu () in
     reductions_menu_item#set_submenu reductions;
     tactics_menu_item#set_submenu tactics;
+    hyperlinks_menu_item#set_submenu hyperlinks;
     let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
     let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
     let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in
+    (match element with 
+    | None -> hyperlinks_menu_item#misc#set_sensitive false
+    | Some elt -> 
+        match hrefs_of_elt elt, href_callback with
+        | Some l, Some f ->
+            List.iter 
+              (fun h ->
+                let item = add_menu_item ~menu:hyperlinks ~label:h () in
+                connect_menu_item item (fun () -> f h)) l
+        | _ -> hyperlinks_menu_item#misc#set_sensitive false);
     menu#append (GMenu.separator_item ());
     let copy = add_menu_item ~stock:`COPY () in
     let gui = get_gui () in
@@ -329,9 +365,10 @@ object (self)
           (match self#get_element_at x y with
           | None -> ()
           | Some elt ->
+              if has_maction elt then ignore(self#action_toggle elt) else
               (match hrefs_of_elt elt with
               | Some hrefs -> self#invoke_href_callback hrefs gdk_button
-              | None -> ignore (self#action_toggle elt)))
+              | None -> ()))
     end;
     false
 
@@ -1134,12 +1171,24 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private tex () =
       let b = Buffer.create 1000 in
+      Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n";
+      List.iter 
+        (fun l ->
+           List.iter (fun sym ->
+             Printf.bprintf b "  %s" (Glib.Utf8.from_unichar sym) 
+           ) l;
+           Printf.bprintf b "\n";
+        )
+        (List.sort 
+          (fun l1 l2 -> compare (List.hd l1) (List.hd l2))
+          (Virtuals.get_all_eqclass ()));
+      Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n";
       List.iter 
         (fun tag, items -> 
-           Printf.bprintf b "%s:\n" tag;
+           Printf.bprintf b "  %s:\n" tag;
            List.iter 
              (fun names, symbol ->
-                Printf.bprintf b "\t%s\t%s\n" 
+                Printf.bprintf b "  \t%s\t%s\n" 
                   (Glib.Utf8.from_unichar symbol)
                   (String.concat ", " names))
              (List.sort