X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=f57dc4d320824cd2e67fb213a5368c5dd596c16a;hb=2aaccff18bc81943efe0c1b76dbe4613f93de5bc;hp=e6c26179132205f9028779dc0a8d7868b9271f43;hpb=65aa5d46b240da7b91e57fc74890d8544aa479c3;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index e6c261791..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
 
@@ -1102,15 +1139,21 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       Lazy.force load_easter_egg
 
     method private redraw_gviz ?center_on () =
-      let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in
-      let fmt = Format.formatter_of_out_channel oc in
-      MetadataDeps.DepGraph.render fmt gviz_graph;
-      close_out oc;
-      gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
-      (match center_on with
-      | None -> ()
-      | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri));
-      HExtlib.safe_remove tmpfile
+      if Sys.command "which dot" = 0 then
+       let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in
+       let fmt = Format.formatter_of_out_channel oc in
+       MetadataDeps.DepGraph.render fmt gviz_graph;
+       close_out oc;
+       gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
+       (match center_on with
+       | None -> ()
+       | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri));
+       HExtlib.safe_remove tmpfile
+      else
+       MatitaGtkMisc.report_error ~title:"graphviz error"
+        ~message:("Graphviz is not installed but is necessary to render "^
+         "the graph of dependencies amoung objects. Please install it.")
+        ~parent:win#toplevel ()
 
     method private dependencies direction uri () =
       let dbd = LibraryDb.instance () in
@@ -1127,19 +1170,35 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showGviz
 
     method private tex () =
-      let text = String.concat "\n"
-        (List.map (fun (k,vs) -> 
-           let vs = 
-             List.sort (fun a b -> String.length a - String.length b) vs
-           in
-           let vs = 
-             if List.length vs < 4 then vs else 
-             let vs, _ = HExtlib.split_nth 4 vs in vs
-           in
-           k ^ "\t" ^ String.concat ", " vs)
-        (Utf8Macro.pp_table ())) 
-      in
-      self#_loadText text
+      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;
+           List.iter 
+             (fun names, symbol ->
+                Printf.bprintf b "  \t%s\t%s\n" 
+                  (Glib.Utf8.from_unichar symbol)
+                  (String.concat ", " names))
+             (List.sort 
+               (fun (_,a) (_,b) -> compare a b)
+               items);
+           Printf.bprintf b "\n")
+        (List.sort 
+          (fun (a,_) (b,_) -> compare a b)
+          (Virtuals.get_all_virtuals ()));
+      self#_loadText (Buffer.contents b)
 
     method private _loadText text =
       searchText#source_buffer#set_text text;
@@ -1154,11 +1213,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       match self#script#grafite_status.proof_status with
       | Proof  (uri, metasenv, _subst, bo, ty, attrs) ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
+          let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
           self#_loadObj obj
       | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
+          let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
           self#_loadObj obj
       | _ -> self#blank ()