From c807ee67cbb2406dfb6fd49677ddabf7d5f14a9b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 19 Mar 2008 19:03:22 +0000 Subject: [PATCH] -debug improved --- helm/software/matita/matitaEngine.ml | 2 +- helm/software/matita/matitacLib.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 5f8a1b7a7..8772fd03b 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -154,7 +154,7 @@ let eval_from_stream ~first_statement_only ~include_paths in watch_statuses lexicon_status grafite_status ; false, lexicon_status, grafite_status, (new_statuses @ statuses)) - with exn -> + with exn when (not (Helm_registry.get_bool "matita.debug")) -> raise (EnrichedWithLexiconStatus (exn, lexicon_status)) in if stop then s else loop l g s diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index e5a8efe8f..8808aea22 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -248,13 +248,13 @@ let compile options fname = LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; clean_exit baseuri false - | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) -> + | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) as exn' -> (match exn with | Sys.Break -> HLog.error "user break!" | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> let (x, y) = HExtlib.loc_of_floc floc in HLog.error (sprintf "Parse error at %d-%d: %s" x y err) - | exn when matita_debug -> raise exn + | exn when matita_debug -> raise exn' | exn -> HLog.error (snd (MatitaExcPp.to_string exn))); LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status; pp_times fname false big_bang big_bang_u big_bang_s; -- 2.39.2