From 78e39847d4e846421ccb10cda72f1b690550deb1 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 19 Jul 2006 17:28:20 +0000 Subject: [PATCH] - pipe graphviz markup to tred before generating png/map output to get rid of transitive dependencies - added method center_on_href to clamp viewport so that a given node is visible (actually it is not a real "center"ing ...) --- helm/software/matita/lablGraphviz.ml | 43 +++++++++++++++++++-------- helm/software/matita/lablGraphviz.mli | 3 ++ 2 files changed, 34 insertions(+), 12 deletions(-) diff --git a/helm/software/matita/lablGraphviz.ml b/helm/software/matita/lablGraphviz.ml index 0084c9204..12d302d24 100644 --- a/helm/software/matita/lablGraphviz.ml +++ b/helm/software/matita/lablGraphviz.ml @@ -31,6 +31,7 @@ type attribute = string * string (* pair *) let png_flags = "-Tpng" let map_flags = "-Tcmapx" +let tred_cmd = "tred" (* graphviz transitive reduction filter *) let tempfile () = Filename.temp_file "matita_" "" @@ -39,18 +40,26 @@ class type graphviz_widget = method load_graph_from_file: string -> unit method connect_href: (GdkEvent.Button.t -> (string * string) list -> unit) -> unit + method center_on_href: string -> 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 mk_gviz_cmd flags src_fname dest_fname = + sprintf "cat %s | %s | %s %s > %s" src_fname tred_cmd gviz_cmd flags + dest_fname in let image = GMisc.image ~packing:viewport#add ~xalign:0. ~yalign:0. ~xpad:0 ~ypad:0 () in + 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 object (self) val mutable href_cb = fun _ _ -> () - val mutable map = [] + val mutable map = [] (* list of associative list attr name -> attr value *) initializer ignore (viewport#event#connect#button_press (fun button -> @@ -58,20 +67,21 @@ class graphviz_impl ?packing gviz_cmd = (* 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 -> ()); + (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)); + let rc = Sys.command (mk_gviz_cmd png_flags fname tmp_png) in + if rc <> 0 then + eprintf + ("Graphviz command failed (exit code: %d) on the following graph:\n" + ^^ "%s\n%!") + rc (HExtlib.input_file fname); image#set_file tmp_png; HExtlib.safe_remove tmp_png; let tmp_map = tempfile () in - ignore (Sys.command (sprintf "%s %s %s > %s" - gviz_cmd map_flags fname tmp_map)); + ignore (Sys.command (mk_gviz_cmd map_flags fname tmp_map)); self#load_map tmp_map; HExtlib.safe_remove tmp_map @@ -89,10 +99,6 @@ class graphviz_impl ?packing gviz_cmd = 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 @@ -104,6 +110,19 @@ class graphviz_impl ?packing gviz_cmd = = href_cb <- cb + method center_on_href href = + (*eprintf "Centering viewport on uri %s\n%!" href;*) + let attrs = + List.find + (fun attrs -> + try List.assoc "href" attrs = href with Not_found -> false) + map in + try + let x1, y1, x2, y2 = parse_coords (List.assoc "coords" attrs) in + viewport#hadjustment#clamp_page ~lower:x1 ~upper:x2; + viewport#vadjustment#clamp_page ~lower:y1 ~upper:y2; + with Not_found -> () + method as_image = image method as_viewport = viewport diff --git a/helm/software/matita/lablGraphviz.mli b/helm/software/matita/lablGraphviz.mli index 7dcedbf75..d6b7f4f6e 100644 --- a/helm/software/matita/lablGraphviz.mli +++ b/helm/software/matita/lablGraphviz.mli @@ -49,6 +49,9 @@ class type graphviz_widget = method connect_href: (GdkEvent.Button.t -> attribute list -> unit) -> unit + (** Center the viewport on the node having the given href value, if any *) + method center_on_href: string -> unit + (** {3 low level access to embedded widgets} * Containment hierarchy: * viewport -- 2.39.2