new command eval added

[helm.git] / helm / software / matita / applyTransformation.ml

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index ca73e2baac10b2738622247327fec249fd903517..e1821ed88a2861147c0e4ffe7b544017dccdd280 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -260,11 +260,22 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
       GrafiteTypes.command_error msg
    in
    let map uri =
+      Librarian.time_stamp "AT: BEGIN MAP";
       try
 (* FG: for now the explicit variables must be discharged *)
-        let do_it obj = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in
-        let obj, real = 
-          Ds.discharge_uri discharge_name (discharge_uri style) uri
+        let do_it obj =
+          let r = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in
+          Librarian.time_stamp "AT: END MAP  "; r
+       in
+       let obj, real = 
+          let s = UM.string_of_uri uri in
+          if Str.string_match matita_prefix s 0 then begin
+             Librarian.time_stamp "AT: GETTING OBJECT";
+             let obj, _ = E.get_obj Un.default_ugraph uri in
+             Librarian.time_stamp "AT: DONE          ";
+              obj, true
+          end else
+             Ds.discharge_uri discharge_name (discharge_uri style) uri
        in
        if real then do_it obj else
        let newuri = discharge_uri style uri in
@@ -314,3 +325,15 @@ let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term =
         ~ids_to_inner_sorts ~ids_to_inner_types ?depth "" context annterm 
   in
   String.concat "" (List.map aux script)
+;;
+
+let txt_of_macro ~map_unicode_to_tex metasenv context m =
+   GrafiteAstPp.pp_macro
+     ~term_pp:(txt_of_cic_term ~map_unicode_to_tex 80 metasenv context) 
+     ~lazy_term_pp:(fun (f : Cic.lazy_term) ->
+        let t,metasenv,_ = f context metasenv CicUniv.empty_ugraph in
+        txt_of_cic_term ~map_unicode_to_tex 80 metasenv context t)
+     m
+;;
+
+