X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaEngine.ml;h=133893f0d1e8cf77155f33de2b3d1fa6a0f4db47;hb=66929b8edb58d468a134b648466f3e9c45ba5c0e;hp=9d88777ac1b97b68fee16039d39aa7dcd32d9847;hpb=e1dee095df33ef99ad011bc30eeb256f31ffdf10;p=helm.git

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index 9d88777ac..133893f0d 100644
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -100,27 +100,38 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
 
 exception TryingToAdd of string
 
+let out = ref ignore 
+
+let set_callback f = out := f
+
 let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
  ?do_heavy_checks ?clean_baseuri ?(enforce_no_new_aliases=true)
- lexicon_status grafite_status str cb 
+ ?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb 
 =
  let rec loop lexicon_status grafite_status statuses =
   let loop =
    if first_statement_only then
-    fun _ _ _ -> raise End_of_file
+    fun _ _ statuses -> statuses
    else
     loop
   in
    if prompt then (print_string "matita> "; flush stdout);
-   try
-    let lexicon_status,ast =
-     GrafiteParser.parse_statement ~include_paths str lexicon_status
-    in
+   let cont =
+     try
+       Some (GrafiteParser.parse_statement ~include_paths str lexicon_status)
+     with
+       End_of_file -> None
+   in
+   match cont with
+   | None -> statuses
+   | Some (lexicon_status,ast) ->
      (match ast with
          GrafiteParser.LNone _ ->
+          watch_statuses lexicon_status grafite_status ;
           loop lexicon_status grafite_status
            (((grafite_status,lexicon_status),None)::statuses)
        | GrafiteParser.LSome ast ->
+          !out ast;
           cb grafite_status ast;
           let new_statuses =
            eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
@@ -142,9 +153,8 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
               [] -> assert false
             | (s,_)::_ -> s
           in
+           watch_statuses lexicon_status grafite_status ;
            loop lexicon_status grafite_status (new_statuses @ statuses))
-   with
-    End_of_file -> statuses
  in
   loop lexicon_status grafite_status []
 ;;