X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=d585cfbee7fc15ab4e1aa9bea41333f71ee072a6;hb=ea3b15fdedb39c72ae1b39f210917c6f38fc062d;hp=ca73e2baac10b2738622247327fec249fd903517;hpb=d2d20cd33c42d0897765387042c3779109bbf4fd;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index ca73e2baa..d585cfbee 100644
--- 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