X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaEngine.ml;fp=matitaB%2Fmatita%2FmatitaEngine.ml;h=734140ad3dc6be656045a2be7c3e6b15c513dbc6;hb=3800a841aa7115b10432f588d31b77129b3a0dc9;hp=14716e2b68143102be55fa187c63ac6349b781fb;hpb=35447b603d9b94a7a05bebc640d61d263820624c;p=helm.git

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 14716e2b6..734140ad3 100644
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -147,28 +147,37 @@ let rec get_ast status ~compiling ~asserted ~include_paths strm =
 
 and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
  let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop asserted status =
-  let asserted,stop,status = 
+ let rec loop asserted status str =
+  let asserted,stop,status,str = 
    try
      let cont =
        try Some (get_ast status ~compiling ~asserted ~include_paths str)
        with End_of_file -> None in
      match cont with
-     | None -> asserted, true, status
+     | None -> asserted, true, status, str
      | Some (asserted,ast) ->
         (* pp_ast_statement status ast; *)
         cb status ast;
         let status =
           eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
         in
-         asserted, false, status
+        let str =
+         match ast with
+            (GrafiteAst.Executable
+              (_,GrafiteAst.NCommand
+                (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
+              GrafiteParser.parsable_statement status
+               (GrafiteParser.strm_of_parsable str)
+          | _ -> str
+        in
+         asserted, false, status, str
    with exn when not matita_debug ->
      prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn);
      raise (EnrichedWithStatus (exn, status))
   in
-  if stop then asserted,status else loop asserted status
+  if stop then asserted,status else loop asserted status str
  in
-  loop asserted status
+  loop asserted status str
 
 and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
   if List.mem fname compiling then raise (CircularDependency fname);