From a7621a29b6d6f4c9c9c3c04e9465ae66c0f5dafd Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 9 Feb 2007 16:05:29 +0000
Subject: [PATCH] The ApplyTransformation.txt_of_term function has been made
 more robust to exceptions.

---
 helm/software/matita/applyTransformation.ml | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 0b03ff080..47e8dd231 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -114,8 +114,23 @@ ignore (
        Sys.Break as exn -> raise exn
      | exn ->
         "[[ Exception raised during pretty-printing: " ^
-        Printexc.to_string exn ^ " ]] " ^
-        CicMetaSubst.ppterm_in_context ~metasenv subst term context)
+         (try
+           Printexc.to_string exn
+          with
+             Sys.Break as exn -> raise exn
+           | _ -> "<<exception raised pretty-printing the exception>>"
+         ) ^ " ]] " ^
+        (CicMetaSubst.use_low_level_ppterm_in_context := true;
+         try
+          let res =
+           CicMetaSubst.ppterm_in_context ~metasenv subst term context
+          in
+           CicMetaSubst.use_low_level_ppterm_in_context := false;
+           res
+         with
+          exc -> 
+           CicMetaSubst.use_low_level_ppterm_in_context := false;
+           raise exc))
 );;
 
 (****************************************************************************)
-- 
2.39.2