]> matita.cs.unibo.it Git - helm.git/commitdiff
The ApplyTransformation.txt_of_term function has been made more robust to
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Feb 2007 16:05:29 +0000 (16:05 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Feb 2007 16:05:29 +0000 (16:05 +0000)
exceptions.

helm/software/matita/applyTransformation.ml

index 0b03ff0804bd687883d9fda335d83eac52214641..47e8dd23162b6d038d36334f3d6715f6bbbdd997 100644 (file)
@@ -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))
 );;
 
 (****************************************************************************)