moved graphviz pretty printer outside matita, so that it can be used by other compone...

diff --git a/components/extlib/.depend b/components/extlib/.depend
index 60d32461b8ff18f78a2e0b32cf334af9b00860e8..bd82a603c1bad2340f31b5601a2f4994c499772f 100644 (file)
--- a/components/extlib/.depend
+++ b/components/extlib/.depend
@@ -12,3 +12,5 @@ trie.cmo: trie.cmi
 trie.cmx: trie.cmi 
 refCounter.cmo: refCounter.cmi 
 refCounter.cmx: refCounter.cmi 
+graphvizPp.cmo: graphvizPp.cmi 
+graphvizPp.cmx: graphvizPp.cmi 

diff --git a/components/extlib/Makefile b/components/extlib/Makefile
index 8caad1fca7d9b7aebff68eac61f26bd1ddbed1c0..25b49280c29cde8883bc688fd32ffdc10b2fe7b4 100644 (file)
--- a/components/extlib/Makefile
+++ b/components/extlib/Makefile
@@ -9,6 +9,7 @@ INTERFACE_FILES =               \
        hLog.mli                \
        trie.mli                \
        refCounter.mli          \
+       graphvizPp.mli          \
        $(NULL)
 IMPLEMENTATION_FILES = \
        $(INTERFACE_FILES:%.mli=%.ml)

diff --git a/components/extlib/graphvizPp.ml b/components/extlib/graphvizPp.ml
new file mode 100644 (file)
index 0000000..18ebd94
--- /dev/null
+++ b/components/extlib/graphvizPp.ml
@@ -0,0 +1,60 @@
+(* Copyright (C) 2006, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+type attribute = string * string  (* <key, value> pair *)
+
+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
+

diff --git a/components/extlib/graphvizPp.mli b/components/extlib/graphvizPp.mli
new file mode 100644 (file)
index 0000000..fa635a9
--- /dev/null
+++ b/components/extlib/graphvizPp.mli
@@ -0,0 +1,44 @@
+(* Copyright (C) 2006, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+(** {2 Pretty printer for generating (textual) Graphviz markup} *)
+
+type attribute = string * string  (* <key, value> pair *)
+
+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
+

diff --git a/matita/lablGraphviz.ml b/matita/lablGraphviz.ml
index ac5cd7537577fa31f2d9b28bb0c2ec6f5cd5f676..0084c9204d64e3a35cd2c57038eb27c2c9f2b5be 100644 (file)
--- a/matita/lablGraphviz.ml
+++ b/matita/lablGraphviz.ml
@@ -118,39 +118,3 @@ 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/matita/lablGraphviz.mli b/matita/lablGraphviz.mli
index c15e580b142199751b8a5bec24571f02803b9311..7dcedbf7547870feab94b187cf033a3a533ee31b 100644 (file)
--- a/matita/lablGraphviz.mli
+++ b/matita/lablGraphviz.mli
@@ -66,23 +66,3 @@ 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
-