X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FlablGraphviz.mli;h=d6b7f4f6ee1a48043dd1151443266052d372e94b;hb=9d5de2f3f3a8921397b939ce2143b22aa71959ea;hp=ca5c7a02b5768856d6401d30cd701bac7dd24962;hpb=c48b5aad2194bb8296bfbbb8ba6766bc6e578c2e;p=helm.git

diff --git a/matita/lablGraphviz.mli b/matita/lablGraphviz.mli
index ca5c7a02b..d6b7f4f6e 100644
--- a/matita/lablGraphviz.mli
+++ b/matita/lablGraphviz.mli
@@ -28,6 +28,8 @@
 (** {1 LablGtk "widget" for rendering Graphviz graphs and connecting to clicks
  * on nodes, edges, ...} *)
 
+type attribute = string * string  (* <key, value> pair *)
+
 class type graphviz_widget =
   object
 
@@ -45,7 +47,10 @@ class type graphviz_widget =
      * (e.g.: [ "shape","rect"; "href","http://foo.bar.com/";
      *          "title","foo"; "alt","description"; "coords","41,6,113,54" ] *)
     method connect_href:
-      (GdkEvent.Button.t -> (string * string) list -> unit) -> unit
+      (GdkEvent.Button.t -> attribute list -> unit) -> unit
+
+    (** Center the viewport on the node having the given href value, if any *)
+    method center_on_href: string -> unit
 
       (** {3 low level access to embedded widgets}
        * Containment hierarchy: