From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 6 Apr 2007 11:25:34 +0000 (+0000)
Subject: eval_from_stream is now tail recursive!
X-Git-Tag: make_still_working~6404
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=87f402f2961595a767a88d4bf16f608e034016e3;hp=61c55501b5ef3f3362b65d8172c1b5085594a4c2;p=helm.git

eval_from_stream is now tail recursive!
---

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index 191c60bb1..133893f0d 100644
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -116,10 +116,15 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
     loop
   in
    if prompt then (print_string "matita> "; flush stdout);
-   try
-    let lexicon_status,ast =
-     GrafiteParser.parse_statement ~include_paths str lexicon_status
-    in
+   let cont =
+     try
+       Some (GrafiteParser.parse_statement ~include_paths str lexicon_status)
+     with
+       End_of_file -> None
+   in
+   match cont with
+   | None -> statuses
+   | Some (lexicon_status,ast) ->
      (match ast with
          GrafiteParser.LNone _ ->
           watch_statuses lexicon_status grafite_status ;
@@ -150,8 +155,6 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
           in
            watch_statuses lexicon_status grafite_status ;
            loop lexicon_status grafite_status (new_statuses @ statuses))
-   with
-    End_of_file -> statuses
  in
   loop lexicon_status grafite_status []
 ;;