if not (Helm_registry.get_bool "matita.verbose") then
let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
let r = Unix.gettimeofday () -. big_bang in
if not (Helm_registry.get_bool "matita.verbose") then
let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
let r = Unix.gettimeofday () -. big_bang in
let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
let rc,rcascii =
if rc then "\e[0;32mOK\e[0m","Ok" else "\e[0;31mFAIL\e[0m","Fail" in
let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
let rc,rcascii =
if rc then "\e[0;32mOK\e[0m","Ok" else "\e[0;31mFAIL\e[0m","Fail" in
let include_paths = get_include_paths options in
let root,baseuri,fname,_tgt =
Librarian.baseuri_of_script ~include_paths fname in
let include_paths = get_include_paths options in
let root,baseuri,fname,_tgt =
Librarian.baseuri_of_script ~include_paths fname in
(* cleanup of previously compiled objects *)
if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
LibraryClean.db_uris_of_baseuri baseuri <> [])
(* cleanup of previously compiled objects *)
if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
LibraryClean.db_uris_of_baseuri baseuri <> [])
let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in
print_string s; flush stdout);
(* we dalay this error check until we print 'matitac file ' *)
let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in
print_string s; flush stdout);
(* we dalay this error check until we print 'matitac file ' *)
(* create dir for XML files *)
if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
~default:false)
(* create dir for XML files *)
if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
~default:false)
if proof_status <> GrafiteTypes.No_proof then
(HLog.error
"there are still incomplete proofs at the end of the script";
if proof_status <> GrafiteTypes.No_proof then
(HLog.error
"there are still incomplete proofs at the end of the script";
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
true)
with
(* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
| AttemptToInsertAnAlias lexicon_status ->
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
true)
with
(* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
| AttemptToInsertAnAlias lexicon_status ->
HLog.error (sprintf "Parse error at %d-%d: %s" x y err)
| exn -> HLog.error (snd (MatitaExcPp.to_string exn)));
LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
HLog.error (sprintf "Parse error at %d-%d: %s" x y err)
| exn -> HLog.error (snd (MatitaExcPp.to_string exn)));
LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
clean_exit baseuri false
| exn ->
if matita_debug then raise exn;
HLog.error
("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn));
clean_exit baseuri false
| exn ->
if matita_debug then raise exn;
HLog.error
("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn));