From: Claudio Sacerdoti Coen 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)