From 59ccad1f8e0f2da227dddbcd5214ade4744fd8ba Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 22 Dec 2018 00:05:24 +0100 Subject: [PATCH] Fixes to show coercion graph - new bug in dot avoided (graphviz commands no longer chainable) - avoided bug that printed a broken icon in place of an empty graph; now we print nothing (a cleared pixbuf) which is not white. It would be better to show something to make clear the graph is empty --- matita/matita/lablGraphviz.ml | 17 ++++++++++------- matita/matita/matitaMathView.ml | 8 ++++++-- 2 files changed, 16 insertions(+), 9 deletions(-) diff --git a/matita/matita/lablGraphviz.ml b/matita/matita/lablGraphviz.ml index ab817e294..27835e3e9 100644 --- a/matita/matita/lablGraphviz.ml +++ b/matita/matita/lablGraphviz.ml @@ -74,17 +74,20 @@ class graphviz_impl ?packing () = method load_graph_from_file ?(gviz_cmd = "dot") fname = let tmp_png = tempfile () in let rc = Sys.command (mk_gviz_cmd gviz_cmd png_flags fname tmp_png) in - if rc <> 0 then + if rc <> 0 || (Unix.stat tmp_png).st_size = 0 then begin 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 (mk_gviz_cmd gviz_cmd map_flags fname tmp_map)); - self#load_map tmp_map; - HExtlib.safe_remove tmp_map + image#clear () + end else begin + image#set_file tmp_png; + HExtlib.safe_remove tmp_png; + let tmp_map = tempfile () in + ignore (Sys.command (mk_gviz_cmd gviz_cmd map_flags fname tmp_map)); + self#load_map tmp_map; + HExtlib.safe_remove tmp_map + end method private load_map fname = let areas = ref [] in diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 390257422..ef7780f0c 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -326,10 +326,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) close_out oc; if tred then gviz#load_graph_from_file - ~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename + (* gvpack can no longer read the output of -Txdot :-( *) + (*~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename*) + ~gviz_cmd:"dot -Txdot | tred | dot" filename else gviz#load_graph_from_file - ~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename; + (* gvpack can no longer read the output of -Txdot :-( *) + (*~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename;*) + ~gviz_cmd:"dot -Txdot | dot" filename; HExtlib.safe_remove filename in object (self) -- 2.39.2