X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FlablGraphviz.mli;h=7b90eec12e9c60c486fcb21a286e3e7c3f00d7a5;hb=b637879a2b3f2ceda65afb3c950061189c4730b7;hp=ca5c7a02b5768856d6401d30cd701bac7dd24962;hpb=fb8e346faf0b390cd8e81376e0dad8333547657a;p=helm.git

diff --git a/helm/software/matita/lablGraphviz.mli b/helm/software/matita/lablGraphviz.mli
index ca5c7a02b..7b90eec12 100644
--- a/helm/software/matita/lablGraphviz.mli
+++ b/helm/software/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
 
@@ -36,8 +38,13 @@ class type graphviz_widget =
       *    GtkImage widget
       * 2) render it to a (HTML) map, internalizing its data.
       * Remember that map entries are generated only for nodes, (edges, ...)
-      * that have an "href" (or "URL", a synonym) attribute *)
-    method load_graph_from_file: string -> unit
+      * that have an "href" (or "URL", a synonym) attribute 
+      * Interesting values for gviz_cmd are:
+      *   'neato'
+      *   'dot'
+      *   'tred | dot'
+      *)
+    method load_graph_from_file: ?gviz_cmd:string -> string -> unit
 
     (** Callback invoked when a click on a node listed in the map is received.
      * @param gdk's button event
@@ -45,7 +52,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:
@@ -58,9 +68,5 @@ class type graphviz_widget =
 
 (** {2 Constructors} *)
 
-val gDot: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gNeato: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gTwopi: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gCirco: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gFdp: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
+val graphviz: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget