X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FlablGraphviz.ml;h=ab817e2940394c19a197810fecd79d6d825711f9;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=0084c9204d64e3a35cd2c57038eb27c2c9f2b5be;hpb=68e83da0f741009b8fdcc89934a251eafabc9012;p=helm.git diff --git a/helm/software/matita/lablGraphviz.ml b/helm/software/matita/lablGraphviz.ml index 0084c9204..ab817e294 100644 --- a/helm/software/matita/lablGraphviz.ml +++ b/helm/software/matita/lablGraphviz.ml @@ -36,21 +36,31 @@ let tempfile () = Filename.temp_file "matita_" "" class type graphviz_widget = object - method load_graph_from_file: string -> unit + method load_graph_from_file: ?gviz_cmd:string -> 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 = +class graphviz_impl ?packing () = let viewport = GBin.viewport ?packing () in + let mk_gviz_cmd gviz_cmd flags src_fname dest_fname = + sprintf "cat %s | %s %s > %s" src_fname 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 = + let xys = HExtlib.split ~sep:' ' s in + let xys = List.flatten (List.map (HExtlib.split ~sep:',') xys) in + match List.map float_of_string xys 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,41 +68,67 @@ 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 = + method load_graph_from_file ?(gviz_cmd = "dot") 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 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 gviz_cmd map_flags fname tmp_map)); self#load_map tmp_map; HExtlib.safe_remove tmp_map method private load_map fname = let areas = ref [] in - let p = + let is_rect l = + try List.assoc "shape" l = "rect" with Not_found -> false + in + let is_poly l = + try List.assoc "shape" l = "poly" with Not_found -> false + in + let rectify l = + List.map ( + function "coords",c -> + let xys = HExtlib.split ~sep:' ' c in + let xys = + List.map + (fun s -> + match HExtlib.split ~sep:',' s with + | [x; y] -> int_of_string x, int_of_string y + | _ -> assert false) + xys + in + let xs, ys = List.split xys in + let max_x = string_of_int (List.fold_left max 0 xs) in + let max_y = string_of_int (List.fold_left max 0 ys) in + let min_x = string_of_int (List.fold_left min max_int xs) in + let min_y = string_of_int (List.fold_left min max_int ys) in + "coords", min_x^","^min_y^" "^max_x^","^max_y + | x -> x) l + in + try + let p = XmlPushParser.create_parser { XmlPushParser.default_callbacks with XmlPushParser.start_element = Some (fun elt attrs -> match elt with - | "area" -> areas := attrs :: !areas + | "area" when is_rect attrs -> areas := attrs :: !areas + | "area" when is_poly attrs -> areas := rectify attrs :: !areas | _ -> ()) } in - XmlPushParser.parse p (`File fname); - map <- !areas + XmlPushParser.parse p (`File fname); + map <- !areas + with XmlPushParser.Parse_error _ -> () 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,17 +140,25 @@ class graphviz_impl ?packing gviz_cmd = = href_cb <- cb + method center_on_href href = + (*eprintf "Centering viewport on uri %s\n%!" href;*) + try + let attrs = + List.find + (fun attrs -> + try List.assoc "href" attrs = href with Not_found -> false) + map + in + 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 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" +let graphviz ?packing () = + (new graphviz_impl ?packing () :> graphviz_widget)