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 () ->
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
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
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 ()