From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 8 Feb 2007 16:55:37 +0000 (+0000)
Subject: If a pretty printed term spans on multiple lines, then it is printed after
X-Git-Tag: make_still_working~6471
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1d3ea10488ce2982213b1da9a18420fbb5491409;p=helm.git

If a pretty printed term spans on multiple lines, then it is printed after
a new line and followed by a new line too.
---

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 920d1fef4..0b03ff080 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -105,7 +105,11 @@ ignore (
     try
      let context' = CicMetaSubst.apply_subst_context subst context in
      let term' = CicMetaSubst.apply_subst subst term in
-      txt_of_cic_term 30 metasenv context' term'
+     let res = txt_of_cic_term 30 metasenv context' term' in
+      if String.contains res '\n' then
+       "\n" ^ res ^ "\n"
+      else
+       res
     with
        Sys.Break as exn -> raise exn
      | exn ->