X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2FautProcess.ml;h=0009e021eea3996b1d7843461aea5f2fea2de459;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=c6ef561f0b26c49bf189ff1b984f841b11ced4fb;hpb=2b821e608cc1fceebc13e85867a244fe02edf71e;p=helm.git

diff --git a/helm/software/lambda-delta/automath/autProcess.ml b/helm/software/lambda-delta/automath/autProcess.ml
index c6ef561f0..0009e021e 100644
--- a/helm/software/lambda-delta/automath/autProcess.ml
+++ b/helm/software/lambda-delta/automath/autProcess.ml
@@ -15,39 +15,63 @@ type status = {
    opening  : bool; (* just opened section *)
    reopening: bool; (* just reopened section *)
    closing  : bool; (* just closed section *)
+   explicit : bool; (* just found explicit context *)
+   block    : bool; (* just found block opener *)
    iao      : int;  (* implicit context after opening section *)
    iar      : int;  (* implicit context after reopening section *)
-   iac      : int   (* implicit context after closing section *)
+   iac      : int;  (* implicit context after closing section *)
+   iag      : int   (* implicit context after global statement *)
 }
 
 (* internal functions *******************************************************)
 
+let orc_reset f st =
+   f {st with opening = false; reopening = false; closing = false}
+
+let orc_count f st =
+   let st = if st.opening then {st with iao = succ st.iao} else st in
+   let st = if st.reopening then {st with iar = succ st.iar} else st in
+   let st = if st.closing then {st with iac = succ st.iac} else st in
+   f st
+
+let exp_count f st =
+   let st = 
+      if st.explicit || st.block then st else {st with iag = succ st.iag} 
+   in
+   f st
+
 let proc_section f st = function
    | Some (true, _)  -> f {st with opening = true} 
    | Some (false, _) -> f {st with reopening = true} 
-   | None            -> f {st with closing = true} 
+   | None            -> f {st with closing = true}
 
 let proc_context f st =
-   f {st with opening = false; reopening = false; closing = false} 
+   orc_reset f {st with explicit = true}
 
-let proc_proper f st =
-   let st = if st.opening then {st with iao = succ st.iao} else st in
-   let st = if st.reopening then {st with iar = succ st.iar} else st in
-   let st = if st.closing then {st with iac = succ st.iac} else st in
-   proc_context f st
+let proc_block f st =
+   orc_count (orc_reset f) {st with explicit = false; block = true}
 
-let proc_item f st item = match item with
-   | A.Section section -> proc_section f st section item
-   | A.Context _       -> proc_context f st item  
-   | _                 -> proc_proper f st item
+let proc_global f st =
+   let f st = 
+      orc_count (orc_reset f) {st with explicit = false; block = false}
+   in
+   exp_count f st
 
+let proc_entity f st entity = match entity with
+   | A.Section section -> proc_section f st section entity
+   | A.Context _       -> proc_context f st entity  
+   | A.Block _         -> proc_block f st entity
+   | A.Decl _          -> proc_global f st entity
+   | A.Def _           -> proc_global f st entity
+   
 (* interface functions ******************************************************)
 
 let initial_status = {
-   opening = false; reopening = false; closing = false;
-   iao = 0; iar = 0; iac = 0
+   opening = false; reopening = false; closing = false; 
+   explicit = false; block = false;
+   iao = 0; iar = 0; iac = 0; iag = 0
 }
 
-let process_item = proc_item
+let process_entity = proc_entity
 
-let get_counters f st = f st.iao st.iar st.iac
+let get_counters f st = f st.iao st.iar st.iac st.iag