From 146e4936a93992e7c5821605bffd3e1e47065f0d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 23 May 2007 13:36:39 +0000 Subject: [PATCH] xxx.dot improved --- .../contribs/formal_topology/bin/theory_explorer.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml index be1e107fb..097dacc07 100644 --- a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml +++ b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml @@ -13,6 +13,8 @@ type compound_operator = op list let string_of_cop op = if op = [] then "id" else String.concat "" (List.map string_of_op op) +let dot_of_cop op = "\"" ^ string_of_cop op ^ "\"" + let rec matita_of_cop v = function | [] -> v @@ -40,12 +42,13 @@ let string_of_equivalence_class (repr,others,leq,_) = let dot_of_equivalence_class (repr,others,leq,_) = (if others <> [] then let eq = String.concat " = " (List.map string_of_cop (repr::others)) in - string_of_cop repr ^ "[label=\"" ^ eq ^ "\"];\n" + dot_of_cop repr ^ "[label=\"" ^ eq ^ "\"];" ^ + if !leq = [] then "" else "\n" else "") ^ String.concat "\n" (List.map (function (repr',_,_,_) -> - string_of_cop repr' ^ " -> " ^ string_of_cop repr ^ ";") !leq) + dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ ";") !leq) (* set of equivalence classes *) type set = equivalence_class list @@ -57,11 +60,12 @@ let ps_of_set ?processing s = let ch = open_out "xxx.dot" in output_string ch "digraph G {\n"; output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s)); + output_string ch "\n"; (match processing with None -> () | Some (repr,rel,repr') -> output_string ch - (string_of_cop repr' ^ " -> " ^ string_of_cop repr ^ + (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ " [" ^ (if rel="=" then "arrowhead=none " else "") ^ "style=dashed];\n")); -- 2.39.2