From ed89063fccf02a7a63cae52292e3ff0cc2548731 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Jun 2008 12:02:28 +0000 Subject: [PATCH 1/1] when -debug do not catch --- helm/software/matita/matitaEngine.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 8772fd03b..fa9a0d393 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -108,6 +108,7 @@ let eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks ?(enforce_no_new_aliases=true) ?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb = + let matita_debug = Helm_registry.get_bool "matita.debug" in let rec loop lexicon_status grafite_status statuses = let loop = if first_statement_only then fun _ _ statuses -> statuses @@ -154,7 +155,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 when (not (Helm_registry.get_bool "matita.debug")) -> + with exn when not matita_debug -> raise (EnrichedWithLexiconStatus (exn, lexicon_status)) in if stop then s else loop l g s -- 2.39.2