X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=f1c1f496d200f41a15ea38171e25747e2e08042e;hb=f809c7537eda20a275b17bc1407f0ee446f70356;hp=0b03ff0804bd687883d9fda335d83eac52214641;hpb=1d3ea10488ce2982213b1da9a18420fbb5491409;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 0b03ff080..f1c1f496d 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -70,7 +70,7 @@ let mml_of_cic_object obj =
    (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
   ids_to_inner_sorts,ids_to_inner_types)))
 
-let txt_of_cic_sequent size metasenv sequent =
+let txt_of_cic_sequent ?map_unicode_to_tex size metasenv sequent =
   let unsh_sequent,(asequent,ids_to_terms,
     ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
   =
@@ -81,10 +81,10 @@ let txt_of_cic_sequent size metasenv sequent =
    CicNotationPres.mpres_of_box
     (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
   in
-  BoxPp.render_to_string (function x::_ -> x | _ -> assert false) size
-   pres_sequent
+  BoxPp.render_to_string ?map_unicode_to_tex
+    (function x::_ -> x | _ -> assert false) size pres_sequent
 
-let txt_of_cic_sequent_conclusion size metasenv sequent = 
+let txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv sequent =
   let _,(asequent,_,_,ids_to_inner_sorts,_) = 
     Cic2acic.asequent_of_sequent metasenv sequent 
   in
@@ -92,11 +92,12 @@ let txt_of_cic_sequent_conclusion size metasenv sequent =
   let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in
   let t = TermContentPres.pp_ast t in
   let t = CicNotationPres.render ids_to_uris t in
-  BoxPp.render_to_string (function x::_ -> x | _ -> assert false) size t
+  BoxPp.render_to_string ?map_unicode_to_tex
+    (function x::_ -> x | _ -> assert false) size t
 
-let txt_of_cic_term size metasenv context t = 
+let txt_of_cic_term ?map_unicode_to_tex size metasenv context t = 
   let fake_sequent = (-1,context,t) in
-  txt_of_cic_sequent_conclusion size metasenv fake_sequent 
+  txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv fake_sequent 
 ;;
 
 ignore (
@@ -114,8 +115,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))
 );;
 
 (****************************************************************************)
@@ -124,7 +140,7 @@ ignore (
 let remove_closed_substs s =
     Pcre.replace ~pat:"{...}" ~templ:"" s
 
-let term2pres n ids_to_inner_sorts annterm = 
+let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm = 
    let ast, ids_to_uris = 
       TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
    in
@@ -136,14 +152,14 @@ let term2pres n ids_to_inner_sorts annterm =
    in
    let render = function _::x::_ -> x | _ -> assert false in
    let mpres = CicNotationPres.mpres_of_box bobj in
-   let s = BoxPp.render_to_string render n mpres in
+   let s = BoxPp.render_to_string ?map_unicode_to_tex render n mpres in
    remove_closed_substs s
 
-let txt_of_cic_object n style prefix obj =
+let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
   let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = 
      try Cic2acic.acic_object_of_cic_object obj
      with e -> 
-        let msg = "Cic2ACic: " ^ Printexc.to_string e in
+        let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
 	failwith msg
   in
   match style with
@@ -151,7 +167,9 @@ let txt_of_cic_object n style prefix obj =
         let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
         let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
         remove_closed_substs ("\n\n" ^
-	   BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj)
+	   BoxPp.render_to_string ?map_unicode_to_tex
+            (function _::x::_ -> x | _ -> assert false) n
+            (CicNotationPres.mpres_of_box bobj)
 	)
      | GrafiteAst.Procedural depth ->
         let term_pp = term2pres (n - 8) ids_to_inner_sorts in
@@ -160,7 +178,7 @@ let txt_of_cic_object n style prefix obj =
         let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in
         let script = Acic2Procedural.acic2procedural 
 	   ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in
-	"\n\n" ^ String.concat "" (List.map aux script)
+	"\n" ^ String.concat "" (List.map aux script)
 
 let txt_of_inline_macro style suri prefix =
    let dbd = LibraryDb.instance () in   
@@ -173,4 +191,4 @@ let txt_of_inline_macro style suri prefix =
 	    Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
 	    (UriManager.string_of_uri uri) (Printexc.to_string e)
    in
-   String.concat "\n\n" (List.map map sorted_uris)
+   String.concat "" (List.map map sorted_uris)