From: Claudio Sacerdoti Coen 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 + | _ -> "<>" + ) ^ " ]] " ^ + (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)) );; (****************************************************************************)