- added to the cicBrowser support for displaying recursive direct/inverse

  dependencies of a given object. To integrate this with cicBrowser's history
  also added a new URI scheme: metadata:/deps/(forward|backward)/URI, where URI
  is the object URI without the trailing "cic:"
- removed automatic stripping of #xpointer(...) from URIs of inductive types

diff --git a/matita/matita.glade b/matita/matita.glade
index f94406c9253128c39f5bd58a59fe68c1cd519e9b..a2bfd8bf5774368d743cdcdf9e3ee1430c452f03 100644 (file)
--- a/matita/matita.glade
+++ b/matita/matita.glade
@@ -33,6 +33,114 @@
          <property name="homogeneous">False</property>
          <property name="spacing">0</property>
 
+         <child>
+           <widget class="GtkMenuBar" id="menubar2">
+             <property name="visible">True</property>
+             <property name="pack_direction">GTK_PACK_DIRECTION_LTR</property>
+             <property name="child_pack_direction">GTK_PACK_DIRECTION_LTR</property>
+
+             <child>
+               <widget class="GtkMenuItem" id="BrowserFileMenu">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">_File</property>
+                 <property name="use_underline">True</property>
+
+                 <child>
+                   <widget class="GtkMenu" id="BrowserFileMenu_menu">
+
+                     <child>
+                       <widget class="GtkImageMenuItem" id="BrowserNewMenuItem">
+                         <property name="visible">True</property>
+                         <property name="label">gtk-new</property>
+                         <property name="use_stock">True</property>
+                       </widget>
+                     </child>
+
+                     <child>
+                       <widget class="GtkSeparatorMenuItem" id="separatormenuitem1">
+                         <property name="visible">True</property>
+                       </widget>
+                     </child>
+
+                     <child>
+                       <widget class="GtkImageMenuItem" id="BrowserCloseMenuItem">
+                         <property name="visible">True</property>
+                         <property name="label">gtk-close</property>
+                         <property name="use_stock">True</property>
+                       </widget>
+                     </child>
+                   </widget>
+                 </child>
+               </widget>
+             </child>
+
+             <child>
+               <widget class="GtkMenuItem" id="BrowserEditMenu">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">_Edit</property>
+                 <property name="use_underline">True</property>
+
+                 <child>
+                   <widget class="GtkMenu" id="BrowserEditMenu_menu">
+
+                     <child>
+                       <widget class="GtkImageMenuItem" id="BrowserCopyMenuItem">
+                         <property name="visible">True</property>
+                         <property name="label">gtk-copy</property>
+                         <property name="use_stock">True</property>
+                       </widget>
+                     </child>
+                   </widget>
+                 </child>
+               </widget>
+             </child>
+
+             <child>
+               <widget class="GtkMenuItem" id="BrowserViewMenu">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">_View</property>
+                 <property name="use_underline">True</property>
+
+                 <child>
+                   <widget class="GtkMenu" id="BrowserViewMenu_menu">
+
+                     <child>
+                       <widget class="GtkMenuItem" id="BrowserMetadataMenuItem">
+                         <property name="visible">True</property>
+                         <property name="label" translatable="yes">_Metadata</property>
+                         <property name="use_underline">True</property>
+                       </widget>
+                     </child>
+
+                     <child>
+                       <widget class="GtkMenuItem" id="DepGraphMenuItem">
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">View the graph of objects on which the current one depends on</property>
+                         <property name="label" translatable="yes">(Direct) Dependencies</property>
+                         <property name="use_underline">True</property>
+                       </widget>
+                     </child>
+
+                     <child>
+                       <widget class="GtkMenuItem" id="InvDepGraphMenuItem">
+                         <property name="visible">True</property>
+                         <property name="tooltip" translatable="yes">View the graph of objects which depends on the current one</property>
+                         <property name="label" translatable="yes">(Inverse) Dependencies</property>
+                         <property name="use_underline">True</property>
+                       </widget>
+                     </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="GtkFrame" id="frame2">
              <property name="visible">True</property>

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 61f184584254256a30716d818eeda019814b26ba..c235a9f4354402669ac495ea0f500f2064945504 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -787,9 +787,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
   in
   let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
+  let metadata_RE = Pcre.regexp "^metadata:/(deps)/(forward|backward)/(.*)$" in
   let whelp_query_RE = Pcre.regexp
     "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$" 
   in
+  let is_metadata txt = Pcre.pmatch ~rex:metadata_RE txt in
   let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
@@ -842,7 +844,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   in
   let load_coerchgraph () = 
       let str = CoercGraph.generate_dot_file () in
-      let filename, oc = Filename.open_temp_file "xx" ".dot" in
+      let filename, oc = Filename.open_temp_file "matita" ".dot" in
       output_string oc str;
       close_out oc;
       gviz#load_graph_from_file filename;
@@ -853,6 +855,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     
     (* Whelp bar queries *)
 
+    val mutable gviz_graph = MetadataDeps.DepGraph.dummy
+    val mutable gviz_uri = UriManager.uri_of_string "cic:/dummy.con";
+
+    val dep_contextual_menu = GMenu.menu ()
+
     initializer
       activate_combo_query "" "locate";
       win#whelpBarComboVbox#add combo#coerce;
@@ -899,14 +906,57 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       mathView#set_href_callback (Some (fun uri ->
         handle_error (fun () ->
           self#load (`Uri (UriManager.uri_of_string uri)))));
-      gviz#connect_href (fun _ attrs ->
+      gviz#connect_href (fun button_ev attrs ->
+        let time = GdkEvent.Button.time button_ev in
         let uri = List.assoc "href" attrs in
-        self#load (`Uri (UriManager.uri_of_string uri)));
+        gviz_uri <- UriManager.uri_of_string uri;
+        match GdkEvent.Button.button button_ev with
+        | button when button = left_button -> self#load (`Uri gviz_uri)
+        | button when button = right_button ->
+            dep_contextual_menu#popup ~button ~time
+        | _ -> ());
+      connect_menu_item win#depGraphMenuItem (fun () ->
+        match self#currentCicUri with
+        | Some uri -> self#load (`Metadata (`Deps (`Fwd, uri)))
+        | None -> ());
+      connect_menu_item win#invDepGraphMenuItem (fun () ->
+        match self#currentCicUri with
+        | Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
+        | None -> ());
+
+      (* fill dep graph contextual menu *)
+      let go_menu_item =
+        GMenu.image_menu_item ~label:"Browse it"
+          ~packing:dep_contextual_menu#append () in
+      let expand_menu_item =
+        GMenu.image_menu_item ~label:"Expand"
+          ~packing:dep_contextual_menu#append () in
+      let collapse_menu_item =
+        GMenu.image_menu_item ~label:"Collapse"
+          ~packing:dep_contextual_menu#append () in
+      dep_contextual_menu#append (go_menu_item :> GMenu.menu_item);
+      dep_contextual_menu#append (expand_menu_item :> GMenu.menu_item);
+      dep_contextual_menu#append (collapse_menu_item :> GMenu.menu_item);
+      connect_menu_item go_menu_item (fun () -> self#load (`Uri gviz_uri));
+      connect_menu_item expand_menu_item (fun () ->
+        MetadataDeps.DepGraph.expand gviz_uri gviz_graph;
+        self#redraw_gviz ~center_on:gviz_uri ());
+      connect_menu_item collapse_menu_item (fun () ->
+        MetadataDeps.DepGraph.collapse gviz_uri gviz_graph;
+        self#redraw_gviz ~center_on:gviz_uri ());
+
       self#_load (`About `Blank);
       toplevel#show ()
 
     val mutable current_entry = `About `Blank 
 
+      (** @return None if no object uri can be built from the current entry *)
+    method private currentCicUri =
+      match current_entry with
+      | `Uri uri
+      | `Metadata (`Deps (_, uri)) -> Some uri
+      | _ -> None
+
     val model =
       new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
 
@@ -976,6 +1026,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
           | `Dir dir -> self#_loadDir dir
+          | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
+              self#dependencies dir uri ()
           | `Uri uri -> self#_loadUriManagerUri uri
           | `Whelp (query, results) -> 
               set_whelp_query query;
@@ -996,9 +1048,30 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       win#mathOrListNotebook#goto_page 2;
       Lazy.force load_easter_egg
 
+    method private redraw_gviz ?center_on () =
+      let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in
+      let fmt = Format.formatter_of_out_channel oc in
+      MetadataDeps.DepGraph.render fmt gviz_graph;
+      close_out oc;
+      gviz#load_graph_from_file tmpfile;
+      (match center_on with
+      | None -> ()
+      | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri));
+      HExtlib.safe_remove tmpfile
+
+    method private dependencies direction uri () =
+      let dbd = LibraryDb.instance () in
+      let graph =
+        match direction with
+        | `Fwd -> MetadataDeps.DepGraph.direct_deps ~dbd uri
+        | `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
+
     method private coerchgraph () =
-      win#mathOrListNotebook#goto_page 3;
-      load_coerchgraph ()
+      load_coerchgraph ();
+      win#mathOrListNotebook#goto_page 3
 
     method private home () =
       self#_showMath;
@@ -1064,19 +1137,31 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     (**  this is what the browser does when you enter a string an hit enter *)
     method loadInput txt =
+      let parse_metadata s =
+        let subs = Pcre.extract ~rex:metadata_RE s in
+        let uri = UriManager.uri_of_string ("cic:/" ^ subs.(3)) in
+        match subs.(1), subs.(2) with
+        | "deps", "forward" -> `Deps (`Fwd, uri)
+        | "deps", "backward" -> `Deps (`Back, uri)
+        | _ -> assert false
+      in
       let txt = HExtlib.trim_blanks txt in
+      (* (* ZACK: what the heck? *)
       let fix_uri txt =
         UriManager.string_of_uri
           (UriManager.strip_xpointer (UriManager.uri_of_string txt))
       in
+      *)
       if is_whelp txt then begin
         set_whelp_query txt;  
         (MatitaScript.current ())#advance ~statement:(txt ^ ".") ()
       end else begin
         let entry =
           match txt with
-          | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt))
+          | txt when is_uri txt ->
+              `Uri (UriManager.uri_of_string ((*fix_uri*) txt))
           | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
+          | txt when is_metadata txt -> `Metadata (parse_metadata txt)
           | txt ->
              (try
                MatitaTypes.entry_of_string txt

diff --git a/matita/matitaTypes.ml b/matita/matitaTypes.ml
index 5e2e98062b4e2c0148783d22d1da9e780e01a64a..177cfb3af42ac179331ffc07ddb524c88d68b3fd 100644 (file)
--- a/matita/matitaTypes.ml
+++ b/matita/matitaTypes.ml
@@ -43,6 +43,7 @@ type mathViewer_entry =
   | `Check of string (* term *)
   | `Cic of Cic.term * Cic.metasenv
   | `Dir of string (* "directory" in cic uris namespace *)
+  | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ]
   | `Uri of UriManager.uri (* cic object uri *)
   | `Whelp of string * UriManager.uri list (* query and results *)
   ]
@@ -55,6 +56,16 @@ let string_of_entry = function
   | `Check _ -> "check:"
   | `Cic (_, _) -> "term:"
   | `Dir uri -> uri
+  | `Metadata meta ->
+      "metadata:/" ^
+      (match meta with
+      | `Deps (dir, uri) ->
+          "deps/" ^
+          let suri =
+            let suri = UriManager.string_of_uri uri in
+            let len = String.length suri in
+            String.sub suri 4 (len - 4) in (* strip "cic:" prefix *)
+          (match dir with | `Fwd -> "forward" | `Back -> "backward") ^ suri)
   | `Uri uri -> UriManager.string_of_uri uri
   | `Whelp (query, _) -> query
 

diff --git a/matita/matitaTypes.mli b/matita/matitaTypes.mli
index 78e0c25415a788907de205a24930049f5576679c..37917d56667bff3dff49c1278face1bf839d5aaa 100644 (file)
--- a/matita/matitaTypes.mli
+++ b/matita/matitaTypes.mli
@@ -32,6 +32,7 @@ type mathViewer_entry =
   | `Check of string
   | `Cic of Cic.term * Cic.metasenv
   | `Dir of string
+  | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ]
   | `Uri of UriManager.uri
   | `Whelp of string * UriManager.uri list ]