- bug fix in the RTM

[helm.git] / helm / software / helena / src / toplevel / top.ml

diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index e7f9158b1e05a8601cba1a517d091a7eac7fe342..d57c2b007555263664213196bd1b8dfc6ba3c887 100644 (file)
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -17,6 +17,7 @@ module C  = Cps
 module L  = Log
 module Y  = Time
 module G  = Options
+module J  = Marks
 module H  = Hierarchy
 module N  = Layer
 module E  = Entity
@@ -128,17 +129,17 @@ let validate st k =
    let brg_err msg = brg_error st "Validation Error" msg; failwith "Interrupted" in
    let ok _ = st in
    match k with
-      | BrgEntity entity -> 
-         let st = BU.validate brg_err ok st.kst entity in
-         begin match st.och with
-            | None     -> st
-            | Some och -> 
-               if BG.output_entity st.kst och entity then st
-               else begin L.warn level "Matita exportation stopped"; {st with och = None} end
-         end
+      | BrgEntity entity -> BU.validate brg_err ok st.kst entity
       | BagEntity _      -> st
       | CrgEntity _      -> st
 
+let grafite st och = function
+   | BrgEntity entity -> 
+      if BG.output_entity st.kst och entity then st else
+      begin L.warn level "Matita exportation stopped"; {st with och = None} end
+   | BagEntity _      -> st
+   | CrgEntity _      -> st
+
 (* extended lexer ***********************************************************)
 
 type 'token lexer = {
@@ -220,11 +221,15 @@ let streaming = ref false (* parsing style (temporary) *)
 
 let process_2 st entity =
    let st = if !G.summary then count_entity st entity else st in
+   let st = 
+      if !G.stage >= 3 then 
+         let f = if !version then validate else type_check in f st entity
+      else st
+   in
    if !export then export_entity st entity;
-   if !G.stage >= 3 then 
-      let f = if !version then validate else type_check in 
-      f st entity
-   else st
+   match st.och with
+     | None     -> st
+     | Some och -> grafite st och entity
 
 let process_1 st entity = 
    if !G.trace >= 3 then pp_progress entity;
@@ -306,7 +311,6 @@ let main =
    let clear_options () =
       export := false; preprocess := false;
       root := "";
-      st := initial_status ();
       G.clear (); H.clear (); O.clear_reductions ();
       streaming := false;
       version := true
@@ -319,6 +323,7 @@ let main =
       if !G.stage <= 1 then G.kernel := G.Crg;
       G.cover := cover;
       if !G.ma_preamble <> "" then st := {!st with och = Some (BG.open_out base_name)};
+      J.clear_marks ();
       let sst, input = process (refresh_status !st) name in
       st := begin match sst.och with 
          | None     -> sst