From 3cdf3d1d9e2ee3c12931c2af5c2daf1b0e73a310 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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. --- helm/software/matita/matitaEngine.ml | 6 ++++-- helm/software/matita/matitaEngine.mli | 1 + 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 9d88777ac..9778f0900 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/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/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli index a03d1e7da..71bfff0b8 100644 --- a/helm/software/matita/matitaEngine.mli +++ b/helm/software/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