X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=329e27e4f8c909251dac4187cd4a87be1ddc64bc;hb=3323758b99384afb5c7a70aa31bc006a78af64dd;hp=1f5b2a22cf76a46965c47aeb7301e03e0c997c8c;hpb=558224e07a053eb99eaba1aed56c686056840dec;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 1f5b2a22c..329e27e4f 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -949,6 +949,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         match self#currentCicUri with
         | Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
         | None -> ());
+      connect_menu_item win#browserCloseMenuItem (fun () ->
+        let my_id = Oo.id self in
+        cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
+        win#toplevel#misc#hide(); win#toplevel#destroy ());
       (* remove hbugs *)
       (*
       connect_menu_item win#hBugsTutorsMenuItem (fun () ->
@@ -1098,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
@@ -1124,7 +1134,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private tex () =
       let text = String.concat "\n"
-        (List.map (fun (k,vs) -> k ^ "\t" ^ String.concat ",  " vs)
+        (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
@@ -1142,11 +1160,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 ()