From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 12 Jul 2006 16:39:03 +0000 (+0000)
Subject: added pretty printer for dot files (it may need to be moved elsewhere in the future)
X-Git-Tag: make_still_working~7077
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e271fd61d46f9fa9b1e007e3bc2dd99cbfe5452a;p=helm.git

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

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index 307f3983a..34bbe6328 100644
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -27,6 +27,7 @@ endif
 # objects for matita (GTK GUI)
 CMOS =				\
 	buildTimeConf.cmo	\
+	lablGraphviz.cmo	\
 	matitaTypes.cmo		\
 	matitaMisc.cmo		\
 	matitamakeLib.cmo	\
@@ -39,7 +40,6 @@ CMOS =				\
 	matitaScript.cmo	\
 	matitaGeneratedGui.cmo	\
 	matitaMathView.cmo 	\
-	lablGraphviz.cmo	\
 	matitaGui.cmo		\
 	$(NULL)
 # objects for matitac (batch compiler)
diff --git a/helm/software/matita/lablGraphviz.ml b/helm/software/matita/lablGraphviz.ml
index d5e06c265..ac5cd7537 100644
--- a/helm/software/matita/lablGraphviz.ml
+++ b/helm/software/matita/lablGraphviz.ml
@@ -27,6 +27,8 @@
 
 open Printf
 
+type attribute = string * string  (* <key, value> pair *)
+
 let png_flags = "-Tpng"
 let map_flags = "-Tcmapx"
 
@@ -116,3 +118,39 @@ let gTwopi = factory "twopi"
 let gCirco = factory "circo"
 let gFdp = factory "fdp"
 
+module Pp =
+  struct
+
+    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
+
+    open Format
+
+    module Dot =
+      struct
+        let attribute fmt (k, v) = fprintf fmt "@[<hv2>%s=@,\"%s\",@]" k v
+        let attributes attrs fmt = List.iter (attribute fmt) attrs
+
+        let header ?(name = "g") fmt = fprintf fmt "@[<hv2>digraph %s {@," name
+        let node name ?(attrs = []) fmt =
+          fprintf fmt "@[<hov2>%s@ [" name;
+          attributes attrs fmt;
+          fprintf fmt "];@]@,"
+        let edge name1 name2 ?(attrs = []) fmt =
+          fprintf fmt "@[<hov2>%s ->@ %s@ [" name1 name2;
+          attributes attrs fmt;
+          fprintf fmt "];@]@,"
+        let raw s fmt = pp_print_string fmt s
+        let trailer fmt = fprintf fmt "@,}@]%!"
+      end
+
+  end
+
diff --git a/helm/software/matita/lablGraphviz.mli b/helm/software/matita/lablGraphviz.mli
index ca5c7a02b..c15e580b1 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
 
@@ -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
+