From fb8e346faf0b390cd8e81376e0dad8333547657a Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 12 Jul 2006 14:44:46 +0000 Subject: [PATCH] added widget for rendering and interacting with graphs generated via graphviz --- helm/software/matita/.depend | 8 +- helm/software/matita/Makefile | 1 + helm/software/matita/lablGraphviz.ml | 117 ++++++++++++++++++++++++++ helm/software/matita/lablGraphviz.mli | 66 +++++++++++++++ 4 files changed, 190 insertions(+), 2 deletions(-) create mode 100644 helm/software/matita/lablGraphviz.ml create mode 100644 helm/software/matita/lablGraphviz.mli diff --git a/helm/software/matita/.depend b/helm/software/matita/.depend index 2c41ea6ef..b893373e1 100644 --- a/helm/software/matita/.depend +++ b/helm/software/matita/.depend @@ -6,6 +6,8 @@ dump_moo.cmo: buildTimeConf.cmi dump_moo.cmx: buildTimeConf.cmx gragrep.cmo: matitaInit.cmi buildTimeConf.cmi gragrep.cmi gragrep.cmx: matitaInit.cmx buildTimeConf.cmx gragrep.cmi +lablGraphviz.cmo: lablGraphviz.cmi +lablGraphviz.cmx: lablGraphviz.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \ @@ -47,9 +49,11 @@ matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ - matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi lablGraphviz.cmi \ + buildTimeConf.cmi matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ - matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx + matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx lablGraphviz.cmx \ + buildTimeConf.cmx matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \ matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmi \ applyTransformation.cmi matitaScript.cmi diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index a126ab8ac..307f3983a 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -39,6 +39,7 @@ 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 new file mode 100644 index 000000000..fab25cba6 --- /dev/null +++ b/helm/software/matita/lablGraphviz.ml @@ -0,0 +1,117 @@ +(* 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$ *) + +open Printf + +let png_flags = "-Tpng" +let map_flags = "-Tcmapx" + +let tempfile () = Filename.temp_file "matita_" "" + +class type graphviz_widget = + object + method load_graph_from_file: string -> unit + method connect_href: + (GdkEvent.Button.t -> (string * string) list -> unit) -> unit + method as_image: GMisc.image + method as_viewport: GBin.viewport + end + +class graphviz_impl ?packing gviz_cmd = + let viewport = GBin.viewport ?packing () in + let image = + GMisc.image ~packing:viewport#add ~xalign:0. ~yalign:0. ~xpad:0 ~ypad:0 () + in + object (self) + val mutable href_cb = fun _ _ -> () + val mutable map = [] + + initializer + ignore (viewport#event#connect#button_press (fun button -> + (*eprintf "x: %f; y: %f;\n%!" (GdkEvent.Button.x button +. viewport#hadjustment#value) (GdkEvent.Button.y button +. viewport#vadjustment#value);*) + (* compute coordinates relative to image origin *) + let x = GdkEvent.Button.x button +. viewport#hadjustment#value in + let y = GdkEvent.Button.y button +. viewport#vadjustment#value in + (try + href_cb button (self#find_href x y) + with Not_found -> ()); + false)) + + method load_graph_from_file fname = + let tmp_png = tempfile () in + ignore (Sys.command (sprintf "%s %s %s > %s" + gviz_cmd png_flags fname tmp_png)); + image#set_file tmp_png; + let tmp_map = tempfile () in + ignore (Sys.command (sprintf "%s %s %s > %s" + gviz_cmd map_flags fname tmp_map)); + self#load_map tmp_map; + HExtlib.safe_remove tmp_png + + method private load_map fname = + let areas = ref [] in + let p = + XmlPushParser.create_parser + { XmlPushParser.default_callbacks with + XmlPushParser.start_element = + Some (fun elt attrs -> + match elt with + | "area" -> areas := attrs :: !areas + | _ -> ()) } in + XmlPushParser.parse p (`File fname); + map <- !areas + + method private find_href x y = + let parse_coords s = + match List.map float_of_string (HExtlib.split ~sep:',' s) with + | [x1; y1; x2; y2 ] -> x1, y1, x2, y2 + | _ -> assert false in + List.find + (fun attrs -> + let x1, y1, x2, y2 = parse_coords (List.assoc "coords" attrs) in + x1 <= x && x <= x2 && y1 <= y && y <= y2) + map + + method connect_href + (cb: GdkEvent.Button.t -> (string * string) list -> unit) + = + href_cb <- cb + + method as_image = image + method as_viewport = viewport + + end + +let factory cmd ?packing () = + (new graphviz_impl ?packing cmd :> graphviz_widget) + +let gDot = factory "dot" +let gNeato = factory "neato" +let gTwopi = factory "twopi" +let gCirco = factory "circo" +let gFdp = factory "fdp" + diff --git a/helm/software/matita/lablGraphviz.mli b/helm/software/matita/lablGraphviz.mli new file mode 100644 index 000000000..ca5c7a02b --- /dev/null +++ b/helm/software/matita/lablGraphviz.mli @@ -0,0 +1,66 @@ +(* 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$ *) + +(** {1 LablGtk "widget" for rendering Graphviz graphs and connecting to clicks + * on nodes, edges, ...} *) + +class type graphviz_widget = + object + + (** Load graphviz markup from file and then: + * 1) render it to PNG, loading the risulting image in the embedded + * 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 + + (** Callback invoked when a click on a node listed in the map is received. + * @param gdk's button event + * @param attrs attributes of the node clicked on, as they appear on the map + * (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 + + (** {3 low level access to embedded widgets} + * Containment hierarchy: + * viewport + * \- image *) + + method as_image: GMisc.image + method as_viewport: GBin.viewport + end + +(** {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.39.2