From 7fc80f3be9d5d5d1d244abfe6fa5d27e57594878 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 9 Oct 2006 09:23:09 +0000 Subject: [PATCH] More work to handle -debug properly. --- matita/matitacLib.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 93d92c577..82a7ca32e 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -63,6 +63,7 @@ let run_script is eval_function = 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 @@ -77,7 +78,8 @@ let run_script is eval_function = | 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 () = @@ -298,7 +300,8 @@ let main ~mode = 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 -- 2.39.2