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

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 58fc19208..d585cfbee 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -240,6 +240,8 @@ let discharge_uri style uri =
    let _, s = List.fold_left replacement (false, s) replacements in 
    UM.uri_of_string s
 
+let discharge_name s = s ^ "_discharged"
+
 let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
    let print_exc = function
       | ProofEngineHelpers.Bad_pattern s as e ->
@@ -248,24 +250,45 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
    in
    let dbd = LibraryDb.instance () in   
    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
+   let error uri e =
+      let msg  = 
+         Printf.sprintf 
+            "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s" 
+            (UM.string_of_uri uri) e
+      in
+      Printf.eprintf "%s\n" msg;
+      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_uri style) uri in
+        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
 	let _lemmas = LS.add_obj GE.refinement_toolkit newuri obj in
 	do_it obj
       with
-         | e -> 
-            let msg = 
-	       Printf.sprintf 
-	          "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s" 
-                  (UM.string_of_uri uri) (print_exc e)
-	    in
-	    Printf.eprintf "%s\n" msg;
-	    GrafiteTypes.command_error msg
+         | TC.TypeCheckerFailure s ->
+	    error uri ("failure  : " ^ Lazy.force s)
+         | TC.AssertFailure s      ->
+	    error uri ("assert   : " ^ Lazy.force s)
+         | E.Object_not_found u    ->
+	    error uri ("not found: " ^ UM.string_of_uri u)
+	 | e                       -> error uri (print_exc e)
    in
    String.concat "" (List.map map sorted_uris)