librarian.ml: now the read_only .moo's are managed "correctly" (i.e. better than...

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

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 7d902d3838ad90f40c309adb90049c530d238770..d585cfbee7fc15ab4e1aa9bea41333f71ee072a6 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -260,15 +260,21 @@ 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 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
+          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
-          else
+          end else
              Ds.discharge_uri discharge_name (discharge_uri style) uri
        in
        if real then do_it obj else