From bf64edcd46b60b863c4d77dc2c31ffe119b9a488 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Oct 2009 09:33:40 +0000 Subject: [PATCH] no mode middle age debug menu --- helm/software/matita/matita.ml | 38 +++++++++++++++++----------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 6a4635c5d..b549ed9cc 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -133,10 +133,18 @@ let _ = Helm_registry.get_bool "matita.debug_menu" then begin gui#main#debugMenu#misc#show (); - let addDebugItem ~label callback = + let addDebugItem label callback = let item = GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label () in - ignore (item#connect#activate callback) in + ignore (item#connect#activate callback) + in + let addDebugCheckbox label ?(init=false) callback = + let item = + GMenu.check_menu_item + ~packing:gui#main#debugMenu_menu#append ~label () in + item#set_active init; + ignore (item#connect#toggled (callback item)) + in let addDebugSeparator () = ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ()) in @@ -191,29 +199,21 @@ let _ = Cic.CurrentProof ("current proof",m,Lazy.force p,ty,[],attrs) | Intermediate _ -> assert false))); addDebugSeparator (); - addDebugItem "disable high level pretty printer" - (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := true); - addDebugItem "enable high level pretty printer" - (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := false); + addDebugCheckbox "high level pretty printer" ~init:true + (fun mi () -> CicMetaSubst.use_low_level_ppterm_in_context := mi#active); addDebugSeparator (); - addDebugItem "enable multiple disambiguation passes (default)" - (fun _ -> MultiPassDisambiguator.only_one_pass := false); - addDebugItem "enable only one disambiguation pass" - (fun _ -> MultiPassDisambiguator.only_one_pass := true); addDebugItem "always show all disambiguation errors" (fun _ -> MatitaGui.all_disambiguation_passes := true); addDebugItem "prune disambiguation errors" (fun _ -> MatitaGui.all_disambiguation_passes := false); addDebugSeparator (); - addDebugItem "enable refiner/unification logging" - (fun _ -> NCicRefiner.debug := true; NCicUnification.debug := true; MultiPassDisambiguator.debug := true); - addDebugItem "disable refiner/unification logging" - (fun _ -> NCicRefiner.debug := false; NCicUnification.debug := false; MultiPassDisambiguator.debug := false); - addDebugSeparator (); - addDebugItem "enable reduction logging" - (fun _ -> NCicReduction.debug := true); - addDebugItem "disable reduction logging" - (fun _ -> NCicReduction.debug := false); + addDebugCheckbox "multiple disambiguation passes" ~init:true + (fun mi () -> MultiPassDisambiguator.only_one_pass := mi#active); + addDebugCheckbox "disambiguation/refiner/unification logging" + (fun mi () -> NCicRefiner.debug := mi#active; NCicUnification.debug := + mi#active; MultiPassDisambiguator.debug := mi#active); + addDebugCheckbox "reduction logging" + (fun mi () -> NCicReduction.debug := mi#active); addDebugSeparator (); addDebugItem "Expand virtuals" (fun _ -> (MatitaScript.current ())#expandAllVirtuals); -- 2.39.2