From f799225a710e609a59e398eb8d6d45dad7c62f61 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 7 Jun 2012 09:20:27 +0000 Subject: [PATCH] New debugging switch in the interface. --- matita/components/ng_disambiguation/nCicDisambiguate.ml | 4 ++-- matita/components/ng_disambiguation/nCicDisambiguate.mli | 2 ++ matita/matita/matita.ml | 4 +++- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index 95d26c073..8e3f26777 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -18,8 +18,8 @@ open DisambiguateTypes module Ast = NotationPt module NRef = NReference -let debug_print s = prerr_endline (Lazy.force s);; -let debug_print _ = ();; +let debug = ref false;; +let debug_print s = if !debug then prerr_endline (Lazy.force s);; let cic_name_of_name = function | Ast.Ident (n, None) -> n diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.mli b/matita/components/ng_disambiguation/nCicDisambiguate.mli index 715be6a85..87bdd348a 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.mli +++ b/matita/components/ng_disambiguation/nCicDisambiguate.mli @@ -11,6 +11,8 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) +val debug : bool ref + val disambiguate_term : #NCicCoercion.status -> context:NCic.context -> diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index 7312602fa..d32f69cf0 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -93,9 +93,11 @@ let init_debugging_menu gui = addDebugSeparator (); addDebugCheckbox "tactics logging" (fun mi () -> NTacStatus.debug := mi#active); + addDebugCheckbox "disambiguation logging" + (fun mi () -> MultiPassDisambiguator.debug := mi#active; NCicDisambiguate.debug := mi#active); addDebugCheckbox "disambiguation/refiner/unification/metasubst logging" (fun mi () -> NCicRefiner.debug := mi#active; NCicUnification.debug := - mi#active; MultiPassDisambiguator.debug := mi#active; NCicMetaSubst.debug := mi#active); + mi#active; MultiPassDisambiguator.debug := mi#active; NCicDisambiguate.debug := mi#active; NCicMetaSubst.debug := mi#active); addDebugCheckbox "reduction logging" (fun mi () -> NCicReduction.debug := mi#active); addDebugSeparator (); -- 2.39.2