let pp_ast_statement =
GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
- ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj
+ ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term)
(** {2 Initialization} *)
in
HLog.debug ("Executing: ``" ^ stm ^ "''"))
in
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
try
let grafite_status'', lexicon_status'' =
match eval_function lexicon_status' grafite_status' is cb with
| End_of_file
| CicNotationParser.Parse_error _ as exn -> raise exn
| exn ->
- HLog.error (snd (MatitaExcPp.to_string exn));
+ if not matita_debug then
+ HLog.error (snd (MatitaExcPp.to_string exn)) ;
raise exn
let fname () =
else
"matitac"
in
- let rc = if rc then "OK" else "FAIL" in
+ let rc = if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
let times =
let fmt t =
let seconds = int_of_float t in
end
else
begin
- let baseuri =
+ let baseuri, _fullpathforfname =
DependenciesParser.baseuri_of_script ~include_paths fname in
let moo_fname =
LibraryMisc.obj_file_of_baseuri
exit 0
end
with
- | Sys.Break ->
+ | Sys.Break as exn ->
+ if matita_debug then raise exn;
HLog.error "user break!";
pp_times fname bench_mode false big_bang;
if mode = `COMPILER then