X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2FmatitaMathView.ml;h=544b4f59539c3868e94b8dda0c2dee5c0d3c982a;hb=5a9445562fe66eb78f7f1a0c3a75c569430c63ac;hp=c235a9f4354402669ac495ea0f500f2064945504;hpb=ae810c1e6bfab5076b18c841da9396a867526498;p=helm.git diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml index c235a9f43..544b4f595 100644 --- a/matita/matitaMathView.ml +++ b/matita/matitaMathView.ml @@ -797,7 +797,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 = @@ -1000,6 +1000,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) *) 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 @@ -1025,6 +1026,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `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 () @@ -1053,7 +1055,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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)); @@ -1067,11 +1069,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `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; @@ -1111,6 +1113,16 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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