added displaying of the dep graph of a development, click action still missing

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index a2bfd8bf5774368d743cdcdf9e3ee1430c452f03..62d991dc2e8113d66a5d9f245ae1b4806a2a6df2 100644 (file)
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -4229,6 +4229,84 @@
            </packing>
          </child>
 
+         <child>
+           <widget class="GtkButton" id="graphButton">
+             <property name="visible">True</property>
+             <property name="can_focus">True</property>
+             <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
+
+             <child>
+               <widget class="GtkAlignment" id="alignment17">
+                 <property name="visible">True</property>
+                 <property name="xalign">0.5</property>
+                 <property name="yalign">0.5</property>
+                 <property name="xscale">0</property>
+                 <property name="yscale">0</property>
+                 <property name="top_padding">0</property>
+                 <property name="bottom_padding">0</property>
+                 <property name="left_padding">0</property>
+                 <property name="right_padding">0</property>
+
+                 <child>
+                   <widget class="GtkHBox" id="hbox26">
+                     <property name="visible">True</property>
+                     <property name="homogeneous">False</property>
+                     <property name="spacing">2</property>
+
+                     <child>
+                       <widget class="GtkImage" id="image908">
+                         <property name="visible">True</property>
+                         <property name="stock">gtk-zoom-fit</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
+                       </widget>
+                       <packing>
+                         <property name="padding">0</property>
+                         <property name="expand">False</property>
+                         <property name="fill">False</property>
+                       </packing>
+                     </child>
+
+                     <child>
+                       <widget class="GtkLabel" id="label27">
+                         <property name="visible">True</property>
+                         <property name="label" translatable="yes">Graph</property>
+                         <property name="use_underline">True</property>
+                         <property name="use_markup">False</property>
+                         <property name="justify">GTK_JUSTIFY_LEFT</property>
+                         <property name="wrap">False</property>
+                         <property name="selectable">False</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
+                         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                         <property name="width_chars">-1</property>
+                         <property name="single_line_mode">False</property>
+                         <property name="angle">0</property>
+                       </widget>
+                       <packing>
+                         <property name="padding">0</property>
+                         <property name="expand">False</property>
+                         <property name="fill">False</property>
+                       </packing>
+                     </child>
+                   </widget>
+                 </child>
+               </widget>
+             </child>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">False</property>
+             <property name="fill">False</property>
+           </packing>
+         </child>
+
          <child>
            <widget class="GtkButton" id="closeButton">
              <property name="visible">True</property>

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 7270603a9636b7ebcd4be445ce9350b0757dfefb..4f36938b5e25d67835a6a60900e05505d420bba6 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/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/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 6976d57e05462fdfca54bd3ff8a1d3470c5fcd23..544b4f59539c3868e94b8dda0c2dee5c0d3c982a 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/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/helm/software/matita/matitaTypes.ml b/helm/software/matita/matitaTypes.ml
index 177cfb3af42ac179331ffc07ddb524c88d68b3fd..239ec6c823af485c91925fdf1d3aca5694e7ef4d 100644 (file)
--- a/helm/software/matita/matitaTypes.ml
+++ b/helm/software/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/helm/software/matita/matitaTypes.mli b/helm/software/matita/matitaTypes.mli
index 37917d56667bff3dff49c1278face1bf839d5aaa..dd89ed79b82ed1783038e8af830c012e67ad51fc 100644 (file)
--- a/helm/software/matita/matitaTypes.mli
+++ b/helm/software/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/helm/software/matita/matitamakeLib.ml b/helm/software/matita/matitamakeLib.ml
index 503ed210f53401414236c2f51eb46d195c7c3cae..75c7e742d068d0f1bd2194f9faa95899cb3c5b64 100644 (file)
--- a/helm/software/matita/matitamakeLib.ml
+++ b/helm/software/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/helm/software/matita/matitamakeLib.mli b/helm/software/matita/matitamakeLib.mli
index 98a46666ecce208c2714a8a337c5b52be4c1f38a..89a5e3b5f1dc9e27f7113f96e0f06bce2a73571e 100644 (file)
--- a/helm/software/matita/matitamakeLib.mli
+++ b/helm/software/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
+