Added parameter first_statement_only to the functions in matitaEngine

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index fa9292c8986a7e7033d48c96f27f755b65c46830..bd240032cbc289d714de0e21eadd104b3611a714 100644 (file)
--- 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 _ _ -> ())