From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 12 Jul 2006 17:15:19 +0000 (+0000)
Subject: use lablGraphviz to render the coercion graph and added a callback to follow hyperlin... 
X-Git-Tag: 0.4.95@7852~1208
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c97fb85c9e568dfb4459a7118fcba2db38f5654c;p=helm.git

use lablGraphviz to render the coercion graph and added a callback to follow hyperlinks there
---

diff --git a/matita/matita.glade b/matita/matita.glade
index 8fc50338f..f94406c92 100644
--- a/matita/matita.glade
+++ b/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/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 10b7470a5..61f184584 100644
--- a/matita/matitaMathView.ml
+++ b/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 () =