From: Stefano Zacchiroli Date: Thu, 21 Sep 2006 09:29:14 +0000 (+0000) Subject: added displaying of the dep graph of a development, click action still missing X-Git-Tag: 0.4.95@7852~1016 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1a613a4c0b68938f0ced6e190adffa805d1b5680;p=helm.git added displaying of the dep graph of a development, click action still missing --- diff --git a/matita/matita.glade b/matita/matita.glade index a2bfd8bf5..62d991dc2 100644 --- a/matita/matita.glade +++ b/matita/matita.glade @@ -4229,6 +4229,84 @@ + + + True + True + GTK_RELIEF_NORMAL + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-zoom-fit + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + Graph + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + + + + 0 + False + False + + + True diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 7270603a9..4f36938b5 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -486,10 +486,19 @@ class gui () = match get_devel_selected () with | None -> () | Some d -> - let clean = locker - (fun () -> MatitamakeLib.publish_development_in_bg refresh d) - in - ignore(clean ()))); + let publish = locker (fun () -> + MatitamakeLib.publish_development_in_bg refresh d) in + ignore(publish ()))); + connect_button develList#graphButton (fun () -> + match get_devel_selected () with + | None -> () + | Some d -> + (match MatitamakeLib.dot_for_development d with + | None -> () + | Some _ -> + let browser = MatitaMathView.cicBrowser () in + browser#load (`Development + (MatitamakeLib.name_for_development d)))); connect_button develList#closeButton (fun () -> develList#toplevel#misc#hide()); ignore(develList#toplevel#event#connect#delete 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 diff --git a/matita/matitaTypes.ml b/matita/matitaTypes.ml index 177cfb3af..239ec6c82 100644 --- a/matita/matitaTypes.ml +++ b/matita/matitaTypes.ml @@ -42,6 +42,7 @@ type mathViewer_entry = [ `About of abouts (* current proof *) | `Check of string (* term *) | `Cic of Cic.term * Cic.metasenv + | `Development of string | `Dir of string (* "directory" in cic uris namespace *) | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] | `Uri of UriManager.uri (* cic object uri *) @@ -55,6 +56,7 @@ let string_of_entry = function | `About `Coercions -> "about:coercions" | `Check _ -> "check:" | `Cic (_, _) -> "term:" + | `Development d -> "devel:/" ^ d | `Dir uri -> uri | `Metadata meta -> "metadata:/" ^ diff --git a/matita/matitaTypes.mli b/matita/matitaTypes.mli index 37917d566..dd89ed79b 100644 --- a/matita/matitaTypes.mli +++ b/matita/matitaTypes.mli @@ -31,6 +31,7 @@ type mathViewer_entry = [ `About of abouts | `Check of string | `Cic of Cic.term * Cic.metasenv + | `Development of string | `Dir of string | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] | `Uri of UriManager.uri diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml index 503ed210f..75c7e742d 100644 --- a/matita/matitamakeLib.ml +++ b/matita/matitamakeLib.ml @@ -33,7 +33,6 @@ let logger = fun mark -> | `Warning -> HLog.warn | `Debug -> HLog.debug | `Message -> HLog.message -;; type development = { root: string ; name: string } @@ -83,7 +82,10 @@ let initialize () = let makefile_for_development devel = let develdir = pool () ^ devel.name in develdir ^ "/makefile" -;; + +let dot_for_development devel = + let dot_fname = pool () ^ devel.name ^ "/depend.dot" in + if Sys.file_exists dot_fname then Some dot_fname else None (* given a dir finds a development that is radicated in it or below *) let development_for_dir dir = @@ -100,7 +102,6 @@ let development_for_dir dir = try Some (List.find (fun d -> is_prefix_of d.root dir) !developments) with Not_found -> None -;; let development_for_name name = try @@ -112,7 +113,6 @@ let dump_development devel = let devel_dir = pool () ^ devel.name in HExtlib.mkdir devel_dir; HExtlib.output_file ~filename:(devel_dir ^ rootfile) ~text:devel.root -;; let list_known_developments () = List.map (fun r -> r.name,r.root) !developments @@ -272,7 +272,6 @@ let mk_maker refresh_cb = let build_development_in_bg ?matita_flags ?(target="all") refresh_cb development = call_make ?matita_flags development target (mk_maker refresh_cb) -;; let clean_development ?matita_flags development = call_make ?matita_flags development "clean" make diff --git a/matita/matitamakeLib.mli b/matita/matitamakeLib.mli index 98a46666e..89a5e3b5f 100644 --- a/matita/matitamakeLib.mli +++ b/matita/matitamakeLib.mli @@ -56,3 +56,6 @@ val root_for_development : development -> string (* gives back the name *) val name_for_development : development -> string +(** @return dot file for a given development, if it exists *) +val dot_for_development : development -> string option +