X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=150ec8de07c5d454ff7781e800ba1e9cb53ac89b;hb=6b61a9e6698a7c1936adf217b599e34e65a5e4c9;hp=3cfaff52637177e736ff14ea6a8a99ac84f94ae5;hpb=55ec3926f6fbb5dba13705659fe94d0db38b2666;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 3cfaff526..150ec8de0 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -48,8 +48,7 @@ let mml_of_cic_sequent metasenv sequent =
   in
   let content_sequent = Acic2content.map_sequent asequent in 
   let pres_sequent = 
-    (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
-  in
+   Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent in
   let xmlpres = mpres_document pres_sequent in
   (Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,
    unsh_sequent,
@@ -72,7 +71,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 ?map_unicode_to_tex 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)
   =
@@ -83,23 +82,26 @@ let txt_of_cic_sequent ?map_unicode_to_tex size metasenv sequent =
    CicNotationPres.mpres_of_box
     (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
   in
-  BoxPp.render_to_string ?map_unicode_to_tex
+  BoxPp.render_to_string ~map_unicode_to_tex
     (function x::_ -> x | _ -> assert false) size pres_sequent
 
-let txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv sequent =
+let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size
+ metasenv sequent =
   let _,(asequent,_,_,ids_to_inner_sorts,_) = 
     Cic2acic.asequent_of_sequent metasenv sequent 
   in
   let _,_,_,t = Acic2content.map_sequent asequent in 
-  let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in
+  let t, ids_to_uris =
+   TermAcicContent.ast_of_acic ~output_type 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 ?map_unicode_to_tex
+  BoxPp.render_to_string ~map_unicode_to_tex
     (function x::_ -> x | _ -> assert false) size 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 ?map_unicode_to_tex size metasenv fake_sequent 
+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 ~map_unicode_to_tex ~output_type:`Term size
+   metasenv fake_sequent 
 ;;
 
 ignore (
@@ -109,7 +111,10 @@ ignore (
      let context' = CicMetaSubst.apply_subst_context subst context in
      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
      let term' = CicMetaSubst.apply_subst subst term in
-     let res = txt_of_cic_term 30 metasenv context' term' in
+     let res =
+      txt_of_cic_term
+       ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+       30 metasenv context' term' in
       if String.contains res '\n' then
        "\n" ^ res ^ "\n"
       else
@@ -143,23 +148,20 @@ ignore (
 let remove_closed_substs s =
     Pcre.replace ~pat:"{...}" ~templ:"" s
 
-let term2pres ?map_unicode_to_tex 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
+    TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in
    let bobj =
       CicNotationPres.box_of_mpres (
          CicNotationPres.render ~prec:90 ids_to_uris 
-            (TermContentPres.pp_ast ast)
-      )
-   in
+            (TermContentPres.pp_ast ast)) in
    let render = function _::x::_ -> x | _ -> assert false in
    let mpres = CicNotationPres.mpres_of_box bobj in
-   let s = BoxPp.render_to_string ?map_unicode_to_tex 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 
- ?map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style prefix obj 
+ ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style prefix obj 
 =
   let get_aobj obj = 
      try   
@@ -183,24 +185,26 @@ let txt_of_cic_object
             ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj 
         in
         remove_closed_substs ("\n\n" ^
-           BoxPp.render_to_string ?map_unicode_to_tex
+           BoxPp.render_to_string ~map_unicode_to_tex
             (function _::x::_ -> x | _ -> assert false) n
             (CicNotationPres.mpres_of_box bobj)
         )
      | G.Procedural depth ->
         let obj = ProceduralOptimizer.optimize_obj obj in
         let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
-        let term_pp = term2pres (n - 8) ids_to_inner_sorts in
+        let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
         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 aux = GrafiteAstPp.pp_statement
+         ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
         let script = 
-    Acic2Procedural.acic2procedural 
-           ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed prefix aobj 
+           Acic2Procedural.acic2procedural 
+              ~ids_to_inner_sorts ~ids_to_inner_types 
+	      ?depth ?skip_thm_and_qed prefix aobj 
   in
-        String.concat "" (List.map aux script) ^ "\n\n"
+        "\n\n" ^ String.concat "" (List.map aux script)
 
-let txt_of_inline_macro style suri prefix =
+let txt_of_inline_uri ~map_unicode_to_tex style suri prefix =
    let print_exc = function
       | ProofEngineHelpers.Bad_pattern s as e ->
            Printexc.to_string e ^ " " ^ Lazy.force s
@@ -209,11 +213,28 @@ let txt_of_inline_macro style suri prefix =
    let dbd = LibraryDb.instance () in   
    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
    let map uri =
-      try txt_of_cic_object 78 style prefix (* FG: mi pare meglio 78 *)
-                            (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
+      try 
+        txt_of_cic_object 
+          ~map_unicode_to_tex 78 style prefix
+          (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
       with
          | e -> 
             Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
             (UriManager.string_of_uri uri) (print_exc e)
    in
    String.concat "" (List.map map sorted_uris)
+
+let txt_of_inline_macro ~map_unicode_to_tex style name prefix =
+   let suri = 
+      if Librarian.is_uri name then name else
+      let include_paths = 
+         Helm_registry.get_list Helm_registry.string "matita.includes"
+      in
+      let _, baseuri, _, _ = 
+         Librarian.baseuri_of_script ~include_paths name
+      in
+      baseuri
+   in
+   txt_of_inline_uri ~map_unicode_to_tex style suri prefix
+   
+