From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 14 Jun 2005 08:11:12 +0000 (+0000)
Subject: Bug fixed: when the final proof_status is not No_proof matitac returns -1.
X-Git-Tag: PRE_STORAGE~39
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a5b348ea4c1088a9e5b057e1831c132041308bd0;p=helm.git

Bug fixed: when the final proof_status is not No_proof matitac returns -1.
---

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index b3767c539..d93002183 100644
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -71,7 +71,8 @@ let run_script fname =
     MatitaLog.debug ("Executing: ``" ^ stm ^ "''")
   in
   try
-    status := MatitaEngine.eval_from_stream !status is cb
+    status := MatitaEngine.eval_from_stream !status is cb ;
+    !status
   with
   | CicTextualParser2.Parse_error (floc,err) ->
      let (x, y) = CicAst.loc_of_floc floc in
@@ -93,7 +94,7 @@ let _ =
    List.iter (fun fname -> 
     let time = Unix.time () in
     MatitaLog.message (sprintf "execution of %s started:" fname);
-    run_script fname;
+    let status = run_script fname in
     let elapsed = Unix.time () -. time in
     let tm = Unix.gmtime elapsed in
     let sec = 
@@ -105,7 +106,20 @@ let _ =
     let hou = 
       if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" 
     in
-    MatitaLog.message 
-      (sprintf "execution of %s completed in %s." fname (hou^min^sec))) scripts;
-    exit(0)
-  with Sys.Break -> exit (-1)
+    let proof_status = status.proof_status in
+    if proof_status <> MatitaTypes.No_proof then
+     begin
+      MatitaLog.error
+       "there are still incomplete proofs at the end of the script";
+      exit(-1)
+     end
+    else
+     begin
+      MatitaLog.message 
+       (sprintf "execution of %s completed in %s." fname (hou^min^sec)) ;
+      exit(0)
+     end
+   ) scripts
+  with Sys.Break ->
+   MatitaLog.error "user break!";
+   exit (-1)