X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;fp=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;h=0c85bb0c5dab51560344bdc7b5189f578860a460;hb=6753156ae1618ef3fc7ff401808f769abd9eb03d;hp=6e6ccfc288e34b0838232020c82574c32babe7f4;hpb=8134330933e377a344b5ee38890198dc0b653428;p=helm.git

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 6e6ccfc28..0c85bb0c5 100644
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -94,6 +94,19 @@ let xlate f st entity = match !kernel, entity with
       let f e = f st (BagEntity e) in Y.xlate f MBag.bag_of_meta e  
    | _, entity         -> f st entity
 
+let pp_progress e =
+   let f a u =
+      let s = U.string_of_uri u in
+      let err () = L.warn (P.sprintf "%s" s) in
+      let f i = L.warn (P.sprintf "[%u] %s" i s) in
+      Y.mark err f a
+   in
+   match e with
+      | DrgEntity e -> Y.common f e
+      | BrgEntity e -> Y.common f e
+      | BagEntity e -> Y.common f e      
+      | MetaEntity e -> Y.common f e
+
 let count_entity st = function
    | MetaEntity e -> {st with mc = count MO.count_entity st.mc e} 
    | BrgEntity e  -> {st with brgc = count BrgO.count_entity st.brgc e}
@@ -134,13 +147,7 @@ let graph = ref (H.graph_of_string C.err C.start "Z2")
 let old = ref false
 
 let process_3 f st a u =
-   if !progress then 
-      let s = U.string_of_uri u in
-      let err () = L.warn (P.sprintf "%s" s); f st in
-      let f i = L.warn (P.sprintf "[%u] %s" i s); f st in
-      Y.mark err f a
-   else
-      f st
+   f st
 
 let process_2 f st entity =
    let st = count_entity st entity in
@@ -148,6 +155,7 @@ let process_2 f st entity =
    if !stage > 2 then type_check (process_3 f) st !si !graph entity else f st
 	    
 let process_1 f st entity = 
+   if !progress then pp_progress entity;
    let st = count_entity st entity in
    if !export && !stage = 1 then export_entity !si !graph !moch entity;
    if !stage > 1 then xlate (process_2 f) st entity else f st