From 1d3ea10488ce2982213b1da9a18420fbb5491409 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 8 Feb 2007 16:55:37 +0000 Subject: [PATCH] If a pretty printed term spans on multiple lines, then it is printed after a new line and followed by a new line too. --- helm/software/matita/applyTransformation.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 -> -- 2.39.2