added pretty printer for dot files (it may need to be moved elsewhere in the future)

[helm.git] / matita / lablGraphviz.mli

diff --git a/matita/lablGraphviz.mli b/matita/lablGraphviz.mli
index ca5c7a02b5768856d6401d30cd701bac7dd24962..c15e580b142199751b8a5bec24571f02803b9311 100644 (file)
--- 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,7 @@ 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
 
       (** {3 low level access to embedded widgets}
        * Containment hierarchy:
@@ -64,3 +66,23 @@ 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
+