X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaEngine.ml;h=191c60bb170356a6a7cceb486c84f4171f6d70e1;hb=38d3574438b4f764ad433915c9733cc73a684b39;hp=9778f09007d0e88a8c99dfffb8c2afd87e875a48;hpb=3cdf3d1d9e2ee3c12931c2af5c2daf1b0e73a310;p=helm.git

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index 9778f0900..191c60bb1 100644
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -100,6 +100,10 @@ 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)
  ?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb 
@@ -122,6 +126,7 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
           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