]> matita.cs.unibo.it Git - helm.git/commitdiff
If a pretty printed term spans on multiple lines, then it is printed after
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 8 Feb 2007 16:55:37 +0000 (16:55 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 8 Feb 2007 16:55:37 +0000 (16:55 +0000)
a new line and followed by a new line too.

helm/software/matita/applyTransformation.ml

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