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: make_still_working~6462
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a7621a29b6d6f4c9c9c3c04e9465ae66c0f5dafd;p=helm.git

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

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))
 );;
 
 (****************************************************************************)