X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaMathView.ml;h=544b4f59539c3868e94b8dda0c2dee5c0d3c982a;hb=fd972f2c23de4c32d1335fb2b27e21854c6eb806;hp=6976d57e05462fdfca54bd3ff8a1d3470c5fcd23;hpb=2499f5fdcf4dbfecc6f4fafe925b24ae76f14be8;p=helm.git diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml index 6976d57e0..544b4f595 100644 --- a/matita/matitaMathView.ml +++ b/matita/matitaMathView.ml @@ -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 () @@ -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