X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2FmatitaMathView.ml;h=4b54f60ac1e7f36bdd355147166e9790f53476fa;hb=219834c0e605004a33cae194f1216c0b877b8ab4;hp=6976d57e05462fdfca54bd3ff8a1d3470c5fcd23;hpb=2499f5fdcf4dbfecc6f4fafe925b24ae76f14be8;p=helm.git diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml index 6976d57e0..4b54f60ac 100644 --- a/matita/matitaMathView.ml +++ b/matita/matitaMathView.ml @@ -550,7 +550,8 @@ object (self) ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None)); if BuildTimeConf.debug then begin - let name = "sequent_viewer.xml" in + let name = + "/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in HLog.debug ("load_sequent: dumping MathML to ./" ^ name); ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()) end; @@ -572,7 +573,8 @@ object (self) self#thaw | _ -> if BuildTimeConf.debug then begin - let name = "cic_browser.xml" in + let name = + "/tmp/cic_browser_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in HLog.debug ("cic_browser: dumping MathML to ./" ^ name); ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()) end; @@ -1000,6 +1002,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 +1028,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 +1071,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 +1115,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