X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2FmatitaMathView.ml;h=544b4f59539c3868e94b8dda0c2dee5c0d3c982a;hb=1c139ae493f874bfadb11dd2b8c765d0053ba1f7;hp=5de25e45b13b784bca64eb50c5fafbe7d7341f99;hpb=f80a8edd258a2ca7fa27d8fbccafc11625460455;p=helm.git

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 5de25e45b..544b4f595 100644
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -246,7 +246,6 @@ object (self)
         | _ -> leave_href ())
     | None -> leave_href ()
 
-
   method private tactic_text_pattern_of_node node =
    let id = id_of_node node in
    let cic_info, unsh_sequent = self#get_cic_info id in
@@ -259,6 +258,16 @@ object (self)
        | Some hyp_name -> None, [ hyp_name, text ], None)
    | SelHyp (hyp_name, _ctxt) -> None, [ hyp_name, "%" ], None
 
+  method private tactic_text_of_node node =
+   let id = id_of_node node in
+   let cic_info, unsh_sequent = self#get_cic_info id in
+   match self#get_term_by_id cic_info id with
+   | SelTerm (t, father_hyp) ->
+       let sequent = self#sequent_of_id ~paste_kind:`Term id in
+       let text = self#string_of_cic_sequent sequent in
+       text
+   | SelHyp (hyp_name, _ctxt) -> hyp_name
+
     (** @return a pattern structure which contains pretty printed terms *)
   method private tactic_text_pattern_of_selection =
     match self#get_selections with
@@ -420,10 +429,13 @@ object (self)
   method private string_of_node ~(paste_kind:paste_kind) node =
     if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds
     then
-     let tactic_text_pattern =  self#tactic_text_pattern_of_node node in
-      GrafiteAstPp.pp_tactic_pattern
-       ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false)
-       tactic_text_pattern
+      match paste_kind with
+      | `Pattern ->
+          let tactic_text_pattern =  self#tactic_text_pattern_of_node node in
+          GrafiteAstPp.pp_tactic_pattern
+            ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false)
+            tactic_text_pattern
+      | `Term -> self#tactic_text_of_node node
     else string_of_dom_node node
 
   method private string_of_cic_sequent cic_sequent =
@@ -571,8 +583,8 @@ end
 let tab_label meta_markup =
   let rec aux =
     function
-    | `Current m -> sprintf "<b>%s</b>" (aux m)
     | `Closed m -> sprintf "<s>%s</s>" (aux m)
+    | `Current m -> sprintf "<b>%s</b>" (aux m)
     | `Shift (pos, m) -> sprintf "|<sub>%d</sub>: %s" pos (aux m)
     | `Meta n -> sprintf "?%d" n
   in
@@ -694,7 +706,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         ~env:(fun depth tag (pos, sw) ->
           let markup =
             match depth, pos with
-            | 0, _ -> `Current (render_switch sw)
+            | 0, 0 -> `Current (render_switch sw)
+            | 0, _ -> `Shift (pos, `Current (render_switch sw))
             | 1, pos when Stack.head_tag stack = `BranchTag ->
                 `Shift (pos, render_switch sw)
             | _ -> render_switch sw
@@ -774,14 +787,17 @@ 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
   let gui = get_gui () in
   let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
+  let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
   let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
   let combo,_ = GEdit.combo_box_text ~strings:queries () in
   let activate_combo_query input q =
@@ -824,13 +840,26 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
   let load_easter_egg = lazy (
-    win#easterEggImage#set_file (MatitaMisc.image_path "meegg.png"))
+    win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
+  in
+  let load_coerchgraph () = 
+      let str = CoercGraph.generate_dot_file () in
+      let filename, oc = Filename.open_temp_file "matita" ".dot" in
+      output_string oc str;
+      close_out oc;
+      gviz#load_graph_from_file filename;
+      HExtlib.safe_remove filename
   in
   object (self)
     inherit scriptAccessor
     
     (* 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;
@@ -877,11 +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 button_ev attrs ->
+        let time = GdkEvent.Button.time button_ev in
+        let uri = List.assoc "href" attrs in
+        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
 
@@ -925,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
@@ -940,15 +1016,20 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       * @param uri string *)
     method private _load ?(force=false) entry =
       handle_error (fun () ->
-       if entry <> current_entry || entry = `About `Current_proof || force then
+       if entry <> current_entry || entry = `About `Current_proof || entry =
+         `About `Coercions || force then
         begin
           (match entry with
           | `About `Current_proof -> self#home ()
           | `About `Blank -> self#blank ()
           | `About `Us -> self#egg ()
+          | `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 ()
           | `Uri uri -> self#_loadUriManagerUri uri
           | `Whelp (query, results) -> 
               set_whelp_query query;
@@ -969,6 +1050,31 @@ 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 ~gviz_cmd:"tred | dot" 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 ();
+      self#_showGviz
+
+    method private coerchgraph () =
+      load_coerchgraph ();
+      self#_showGviz
+
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with
@@ -1007,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
@@ -1033,19 +1149,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