]> matita.cs.unibo.it Git - helm.git/blob - matita/lablGraphviz.ml
d5e06c26564946746a9fe00799073e46554b45b5
[helm.git] / matita / lablGraphviz.ml
1 (* Copyright (C) 2006, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 open Printf
29
30 let png_flags = "-Tpng"
31 let map_flags = "-Tcmapx"
32
33 let tempfile () = Filename.temp_file "matita_" ""
34
35 class type graphviz_widget =
36   object
37     method load_graph_from_file: string -> unit
38     method connect_href:
39       (GdkEvent.Button.t -> (string * string) list -> unit) -> unit
40     method as_image: GMisc.image
41     method as_viewport: GBin.viewport
42   end
43
44 class graphviz_impl ?packing gviz_cmd =
45   let viewport = GBin.viewport ?packing () in
46   let image =
47     GMisc.image ~packing:viewport#add ~xalign:0. ~yalign:0. ~xpad:0 ~ypad:0 ()
48   in
49   object (self)
50     val mutable href_cb = fun _ _ -> ()
51     val mutable map = []
52
53     initializer
54       ignore (viewport#event#connect#button_press (fun button ->
55         (*eprintf "x: %f; y: %f;\n%!" (GdkEvent.Button.x button +. viewport#hadjustment#value) (GdkEvent.Button.y button +. viewport#vadjustment#value);*)
56         (* compute coordinates relative to image origin *)
57         let x = GdkEvent.Button.x button +. viewport#hadjustment#value in
58         let y = GdkEvent.Button.y button +. viewport#vadjustment#value in
59         (try
60           href_cb button (self#find_href x y)
61         with Not_found -> ());
62         false))
63
64     method load_graph_from_file fname =
65       let tmp_png = tempfile () in
66       ignore (Sys.command (sprintf "%s %s %s > %s"
67         gviz_cmd png_flags fname tmp_png));
68       image#set_file tmp_png;
69       HExtlib.safe_remove tmp_png;
70       let tmp_map = tempfile () in
71       ignore (Sys.command (sprintf "%s %s %s > %s"
72         gviz_cmd map_flags fname tmp_map));
73       self#load_map tmp_map;
74       HExtlib.safe_remove tmp_map
75
76     method private load_map fname =
77       let areas = ref [] in
78       let p =
79         XmlPushParser.create_parser
80           { XmlPushParser.default_callbacks with
81             XmlPushParser.start_element =
82               Some (fun elt attrs ->
83                 match elt with
84                 | "area" -> areas := attrs :: !areas
85                 | _ -> ()) } in
86       XmlPushParser.parse p (`File fname);
87       map <- !areas
88
89     method private find_href x y =
90       let parse_coords s =
91         match List.map float_of_string (HExtlib.split ~sep:',' s) with
92         | [x1; y1; x2; y2 ] -> x1, y1, x2, y2
93         | _ -> assert false in
94       List.find
95         (fun attrs ->
96           let x1, y1, x2, y2 = parse_coords (List.assoc "coords" attrs) in
97           x1 <= x && x <= x2 && y1 <= y && y <= y2)
98         map
99
100     method connect_href
101       (cb: GdkEvent.Button.t -> (string * string) list -> unit)
102     =
103       href_cb <- cb
104
105     method as_image = image
106     method as_viewport = viewport
107
108   end
109
110 let factory cmd ?packing () =
111   (new graphviz_impl ?packing cmd :> graphviz_widget)
112
113 let gDot = factory "dot"
114 let gNeato = factory "neato"
115 let gTwopi = factory "twopi"
116 let gCirco = factory "circo"
117 let gFdp = factory "fdp"
118