MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
go ()
| exn -> MatitaLog.error (Printexc.to_string exn); go ()
+
+let clean_exit n =
+ match !status with
+ None -> exit n
+ | Some status ->
+ let baseuri = MatitaTypes.get_string_option !status "baseuri" in
+ MatitacleanLib.clean_baseuris ~verbose:false [baseuri];
+ exit n
let main ~mode =
Helm_registry.load_from "matita.conf.xml";
begin
MatitaLog.error
"there are still incomplete proofs at the end of the script";
- exit 2
+ clean_exit 2
end
else
begin
| Sys.Break ->
MatitaLog.error "user break!";
if mode = `COMPILER then
- exit ~-1
+ clean_exit ~-1
else
pp_ocaml_mode ()
| MatitaEngine.Drop ->
if mode = `COMPILER then
- exit 1
+ clean_exit 1
else
pp_ocaml_mode ()
| CicTextualParser2.Parse_error (floc,err) ->
let (x, y) = CicAst.loc_of_floc floc in
MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
if mode = `COMPILER then
- exit 1
+ clean_exit 1
else
pp_ocaml_mode ()
-
+ | _ ->
+ if mode = `COMPILER then
+ clean_exit 3
+ else
+ pp_ocaml_mode ()