let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
let gui = get_gui () in
let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
- let gviz = LablGraphviz.gDot ~packing:win#graphScrolledWin#add () in
+ let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
let combo,_ = GEdit.combo_box_text ~strings:queries () in
let activate_combo_query input q =
*)
method private _showMath = win#mathOrListNotebook#goto_page 0
method private _showList = win#mathOrListNotebook#goto_page 1
+ method private _showGviz = win#mathOrListNotebook#goto_page 3
method private back () =
try
| `About `Coercions -> self#coerchgraph ()
| `Check term -> self#_loadCheck term
| `Cic (term, metasenv) -> self#_loadTermCic term metasenv
+ | `Development d -> self#_showDevelDeps d
| `Dir dir -> self#_loadDir dir
| `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
self#dependencies dir uri ()
let fmt = Format.formatter_of_out_channel oc in
MetadataDeps.DepGraph.render fmt gviz_graph;
close_out oc;
- gviz#load_graph_from_file tmpfile;
+ 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));
| `Back -> MetadataDeps.DepGraph.inverse_deps ~dbd uri in
gviz_graph <- graph; (** XXX check this for memory consuption *)
self#redraw_gviz ~center_on:uri ();
- win#mathOrListNotebook#goto_page 3
+ self#_showGviz
method private coerchgraph () =
load_coerchgraph ();
- win#mathOrListNotebook#goto_page 3
+ self#_showGviz
method private home () =
self#_showMath;
win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry);
current_entry <- entry
+ method private _showDevelDeps d =
+ match MatitamakeLib.development_for_name d with
+ | None -> ()
+ | Some devel ->
+ (match MatitamakeLib.dot_for_development devel with
+ | None -> ()
+ | Some fname ->
+ gviz#load_graph_from_file ~gviz_cmd:"tred | dot" fname;
+ self#_showGviz)
+
method private _loadObj obj =
(* showMath must be done _before_ loading the document, since if the
* widget is not mapped (hidden by the notebook) the document is not