From: Stefano Zacchiroli Date: Thu, 13 Jul 2006 09:39:17 +0000 (+0000) Subject: moved graphviz pretty printer outside matita, so that it can be used by other compone... X-Git-Tag: 0.4.95@7852~1207 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4bc69df9d97954207ebb2df142b927676a026e45;p=helm.git moved graphviz pretty printer outside matita, so that it can be used by other components (e.g. from CoercDb to generated coercions graph) --- diff --git a/components/extlib/.depend b/components/extlib/.depend index 60d32461b..bd82a603c 100644 --- 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 8caad1fca..25b49280c 100644 --- 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 index 000000000..18ebd94d9 --- /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 (* 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 "@[%s=@,\"%s\",@]" k v + let attributes attrs fmt = List.iter (attribute fmt) attrs + + let header ?(name = "g") fmt = fprintf fmt "@[digraph %s {@," name + let node name ?(attrs = []) fmt = + fprintf fmt "@[%s@ [" name; + attributes attrs fmt; + fprintf fmt "];@]@," + let edge name1 name2 ?(attrs = []) fmt = + fprintf fmt "@[%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 index 000000000..fa635a971 --- /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 (* 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 ac5cd7537..0084c9204 100644 --- 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 "@[%s=@,\"%s\",@]" k v - let attributes attrs fmt = List.iter (attribute fmt) attrs - - let header ?(name = "g") fmt = fprintf fmt "@[digraph %s {@," name - let node name ?(attrs = []) fmt = - fprintf fmt "@[%s@ [" name; - attributes attrs fmt; - fprintf fmt "];@]@," - let edge name1 name2 ?(attrs = []) fmt = - fprintf fmt "@[%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 c15e580b1..7dcedbf75 100644 --- 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 -