X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FapplyTransformation.ml;h=0b8bbd1bceeddda0750c8209d9f0e0c10e8303e0;hb=b3779638cd49747f4b71784fba57cfb0a56297f5;hp=b5aa06f9d1d87ffd0e74b3a5023884af3be90b1c;hpb=bda4b3ee9d66b253b258da06cea8b801924b2fe7;p=helm.git

diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml
index b5aa06f9d..0b8bbd1bc 100644
--- a/matita/applyTransformation.ml
+++ b/matita/applyTransformation.ml
@@ -158,7 +158,9 @@ let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm =
    let s = BoxPp.render_to_string ?map_unicode_to_tex render n mpres in
    remove_closed_substs s
 
-let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
+let txt_of_cic_object 
+ ?map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style prefix obj 
+=
   let get_aobj obj = 
      try   
         let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
@@ -186,11 +188,19 @@ let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
         let lazy_term_pp = term_pp in
         let obj_pp = CicNotationPp.pp_obj term_pp in
         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" ^ String.concat "" (List.map aux script)
+	let script = 
+    Acic2Procedural.acic2procedural 
+	   ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed 
+       ?skip_initial_lambdas prefix aobj 
+  in
+	String.concat "" (List.map aux script) ^ "\n\n"
 
 let txt_of_inline_macro style suri prefix =
+   let print_exc = function
+      | ProofEngineHelpers.Bad_pattern s as e ->
+           Printexc.to_string e ^ " " ^ Lazy.force s
+      | e -> Printexc.to_string e
+   in
    let dbd = LibraryDb.instance () in   
    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
    let map uri =
@@ -199,6 +209,6 @@ let txt_of_inline_macro style suri prefix =
       with
          | e -> 
 	    Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
-	    (UriManager.string_of_uri uri) (Printexc.to_string e)
+	    (UriManager.string_of_uri uri) (print_exc e)
    in
    String.concat "" (List.map map sorted_uris)