From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 23 May 2007 13:36:39 +0000 (+0000)
Subject: xxx.dot improved
X-Git-Tag: make_still_working~6324
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=146e4936a93992e7c5821605bffd3e1e47065f0d;hp=99ca90bf28a25fcd1cd84596c37be43c97f74e6e;p=helm.git

xxx.dot improved
---

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"));