From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Jul 2005 13:37:04 +0000 (+0000)
Subject: Pretty printing of the disambiguation environment no longer ends in \n.
X-Git-Tag: V_0_7_2~148
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d83fc9accd4ba44a6296eb707b2f62900380f00a;p=helm.git

Pretty printing of the disambiguation environment no longer ends in \n.
---

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 4df2ab7fb..2547bbdfc 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -49,9 +49,12 @@ let alias_diff ~from status =
 let set_proof_aliases status aliases =
  let new_status = {status with aliases = aliases } in
  let diff = alias_diff ~from:status new_status in
- let moo_content_rev =
-  DisambiguatePp.pp_environment diff ::
-   status.moo_content_rev in
+ let textual_diff =
+  if DisambiguateTypes.Environment.is_empty diff then
+   ""
+  else
+   DisambiguatePp.pp_environment diff ^ "\n" in
+ let moo_content_rev = textual_diff :: status.moo_content_rev in
  {new_status with moo_content_rev = moo_content_rev}
   
 (** given a uri and a type list (the contructors types) builds a list of pairs
diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index 1d36df44d..decaa5f5c 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -42,6 +42,4 @@ let pp_environment env =
         s :: acc)
       env []
   in
-  String.concat "\n" (List.sort compare aliases) ^
-   (if aliases = [] then "" else "\n")
-
+  String.concat "\n" (List.sort compare aliases)