From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 9 Feb 2007 16:05:29 +0000 (+0000)
Subject: The ApplyTransformation.txt_of_term function has been made more robust to
X-Git-Tag: 0.4.95@7852~603
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7f6b2044530540ac8cb1eaec56c0c122a7f8140d;p=helm.git

The ApplyTransformation.txt_of_term function has been made more robust to
exceptions.
---

diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml
index 0b03ff080..47e8dd231 100644
--- a/matita/applyTransformation.ml
+++ b/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))
 );;
 
 (****************************************************************************)