From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Oct 2009 09:33:40 +0000 (+0000)
Subject: no mode middle age debug menu
X-Git-Tag: make_still_working~3327
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bf64edcd46b60b863c4d77dc2c31ffe119b9a488;p=helm.git

no mode middle age debug menu
---

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);