X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fmatita.ml;h=eba59f6fdeabaa95b084c09a2de73379c6c0f847;hb=d00e19c7000a00659ffd609ef79675eb0f010659;hp=5abd0139c920629d155e27ae3f4d9ecabf98dc91;hpb=5858c6b8895010b580b6d7be26a962e7ed74cce4;p=helm.git

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 5abd0139c..eba59f6fd 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,24 +199,23 @@ 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;);
-    addDebugItem "disable refiner/unification logging"
-      (fun _ -> NCicRefiner.debug := false; NCicUnification.debug := false;);
+    addDebugCheckbox "multiple disambiguation passes" ~init:true
+      (fun mi () -> MultiPassDisambiguator.only_one_pass := mi#active);
+    addDebugCheckbox "tactics logging" 
+      (fun mi () -> NTacStatus.debug := 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);