X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FlablGraphviz.mli;h=7b90eec12e9c60c486fcb21a286e3e7c3f00d7a5;hb=dfc523454502ccab6a154a32d1d9b4d941d9a6a0;hp=c15e580b142199751b8a5bec24571f02803b9311;hpb=6f2481585178340b6f174f2db3323f4eb52282ef;p=helm.git

diff --git a/matita/lablGraphviz.mli b/matita/lablGraphviz.mli
index c15e580b1..7b90eec12 100644
--- a/matita/lablGraphviz.mli
+++ b/matita/lablGraphviz.mli
@@ -38,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
@@ -49,6 +54,9 @@ class type graphviz_widget =
     method connect_href:
       (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:
        *  viewport
@@ -60,29 +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
-
-(** {2 Pretty printer for generating Graphviz markup} *)
-
-module Pp:
-  sig
-
-    module type GraphvizFormatter =
-      sig
-        val header: ?name:string -> Format.formatter -> unit
-        val node: string -> ?attrs:(attribute list) -> Format.formatter -> unit
-        val edge:
-          string -> string -> ?attrs:(attribute list) -> Format.formatter ->
-            unit
-        val raw: string -> Format.formatter -> unit
-        val trailer: Format.formatter -> unit
-      end
-
-    module Dot: GraphvizFormatter
-
-  end
+val graphviz: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget