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 920d1fef4bf634075470b586b2db59359cc30549..0b03ff0804bd687883d9fda335d83eac52214641 100644 (file)
--- 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 ->