From a229a988dceead9ffe3ea593fcf98e68a16582cf Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 22 Dec 2005 18:05:32 +0000
Subject: [PATCH] Added parameter first_statement_only to the functions in
 matitaEngine

---
 helm/matita/matitaEngine.ml  | 19 +++++++++++++------
 helm/matita/matitaEngine.mli |  2 ++
 helm/matita/matitacLib.ml    |  4 ++--
 3 files changed, 17 insertions(+), 8 deletions(-)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index fa9292c89..bd240032c 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -86,10 +86,16 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
  in
   ((new_grafite_status,new_lexicon_status),None)::intermediate_states
 
-let eval_from_stream ~include_paths ?(prompt=false) ?do_heavy_checks
- ?clean_baseuri lexicon_status grafite_status str cb 
+let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
+ ?do_heavy_checks ?clean_baseuri 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
+   else
+    loop
+  in
    if prompt then (print_string "matita> "; flush stdout);
    try
     let lexicon_status,ast =
@@ -116,8 +122,9 @@ let eval_from_stream ~include_paths ?(prompt=false) ?do_heavy_checks
   loop lexicon_status grafite_status []
 ;;
 
-let eval_string ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status
- status str
+let eval_string ~first_statement_only ~include_paths ?do_heavy_checks
+ ?clean_baseuri lexicon_status status str
 =
- eval_from_stream ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status
-  status (Ulexing.from_utf8_string str) (fun _ _ -> ())
+ eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks
+  ?clean_baseuri lexicon_status status (Ulexing.from_utf8_string str)
+  (fun _ _ -> ())
diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli
index ddc905db3..a3c54dea6 100644
--- a/helm/matita/matitaEngine.mli
+++ b/helm/matita/matitaEngine.mli
@@ -39,6 +39,7 @@ val eval_ast :
 (* heavy checks slow down the compilation process but give you some interesting
  * infos like if the theorem is a duplicate *)
 val eval_string :
+  first_statement_only:bool ->
   include_paths:string list ->
   ?do_heavy_checks:bool ->
   ?clean_baseuri:bool ->
@@ -50,6 +51,7 @@ val eval_string :
   ) list
 
 val eval_from_stream :
+  first_statement_only:bool ->
   include_paths:string list ->
   ?prompt:bool ->
   ?do_heavy_checks:bool ->
diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index e769fd7d6..7150c6f77 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -112,7 +112,7 @@ let rec interactive_loop () =
   let str = Ulexing.from_utf8_channel stdin in
   try
     run_script str 
-      (MatitaEngine.eval_from_stream ~prompt:true
+      (MatitaEngine.eval_from_stream ~first_statement_only:false ~prompt:true
       ~include_paths:(Helm_registry.get_list Helm_registry.string
         "matita.includes"))
   with 
@@ -180,7 +180,7 @@ let main ~mode =
      Helm_registry.get_list Helm_registry.string "matita.includes" in
     (try
       run_script is 
-       (MatitaEngine.eval_from_stream ~include_paths
+       (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
          ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")))
      with End_of_file -> ());
     let elapsed = Unix.time () -. time in
-- 
2.39.2