From 876455a152c9c4d6b1afcdfbee392210b2ec6b90 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 20 Jan 2007 15:29:51 +0000
Subject: [PATCH] 1. buf fixed in eval_from_stream when
 first_statemente_only=true:    the last computed states were lost 2. added a
 new watcher function to eval_from_stream.    The function is called after the
 execution of each command.

---
 matita/matitaEngine.ml  | 6 ++++--
 matita/matitaEngine.mli | 1 +
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/matita/matitaEngine.ml b/matita/matitaEngine.ml
index 9d88777ac..9778f0900 100644
--- a/matita/matitaEngine.ml
+++ b/matita/matitaEngine.ml
@@ -102,12 +102,12 @@ exception TryingToAdd of string
 
 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
@@ -118,6 +118,7 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
     in
      (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 ->
@@ -142,6 +143,7 @@ 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
diff --git a/matita/matitaEngine.mli b/matita/matitaEngine.mli
index a03d1e7da..71bfff0b8 100644
--- a/matita/matitaEngine.mli
+++ b/matita/matitaEngine.mli
@@ -49,6 +49,7 @@ val eval_from_stream :
   ?do_heavy_checks:bool ->
   ?clean_baseuri:bool ->
   ?enforce_no_new_aliases:bool -> (* default true *)
+  ?watch_statuses:(LexiconEngine.status -> GrafiteTypes.status -> unit) ->
   LexiconEngine.status ->
   GrafiteTypes.status ->
   Ulexing.lexbuf ->
-- 
2.39.2