use lablGraphviz to render the coercion graph and added a callback to follow hyperlin...

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 8fc50338f6590e669c5cea7e1c55d2e4d154a446..f94406c9253128c39f5bd58a59fe68c1cd519e9b 100644 (file)
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -465,6 +465,48 @@
                  <property name="type">tab</property>
                </packing>
              </child>
+
+             <child>
+               <widget class="GtkScrolledWindow" id="GraphScrolledWin">
+                 <property name="visible">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                 <property name="shadow_type">GTK_SHADOW_NONE</property>
+                 <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+                 <child>
+                   <placeholder/>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="tab_expand">False</property>
+                 <property name="tab_fill">True</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkLabel" id="label26">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">Graph</property>
+                 <property name="use_underline">False</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="type">tab</property>
+               </packing>
+             </child>
            </widget>
            <packing>
              <property name="padding">0</property>

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 10b7470a5b463f93661fd40f8a9331be1780e424..61f184584254256a30716d818eeda019814b26ba 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -795,6 +795,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   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.gDot ~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 =
@@ -844,11 +845,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let filename, oc = Filename.open_temp_file "xx" ".dot" in
       output_string oc str;
       close_out oc;
-      let ps = Filename.temp_file "yy" ".png" in
-      ignore (Unix.system ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename));
-      Sys.remove filename;
-      at_exit (fun _ -> Sys.remove ps);
-      win#browserImage#set_file ps
+      gviz#load_graph_from_file filename;
+      HExtlib.safe_remove filename
   in
   object (self)
     inherit scriptAccessor
@@ -901,6 +899,9 @@ 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 ->
+        let uri = List.assoc "href" attrs in
+        self#load (`Uri (UriManager.uri_of_string uri)));
       self#_load (`About `Blank);
       toplevel#show ()
 
@@ -996,7 +997,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       Lazy.force load_easter_egg
 
     method private coerchgraph () =
-      win#mathOrListNotebook#goto_page 2;
+      win#mathOrListNotebook#goto_page 3;
       load_coerchgraph ()
 
     method private home () =