X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=7cb2aa7cbec948ef3cdfbad183f8e959eedd0fb8;hb=81432e2003b9c1514975e006775fe59056e125a4;hp=63cf77a16e356352294078aa27e5651e7213e54c;hpb=cdb3befa0dbcb6754cb67b5aa8faae0677a720ef;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 63cf77a16..7cb2aa7cb 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -1102,15 +1102,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 +1133,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;