From: Claudio Sacerdoti Coen Date: Fri, 21 Dec 2018 23:05:24 +0000 (+0100) Subject: Fixes to show coercion graph X-Git-Tag: make_still_working~229^2~1^2~33 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bd81dfa48a0a2c8c6da42bd62e0357c5ed862179;p=helm.git 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 --- 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)