updating the structures for sorts

[helm.git] / helm / software / matita / matita.ml

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 6a4635c5d6477513caf4097ad8353f854ac79b58..4fdc704e220a8593610a18635bf9f72a37304e23 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -133,16 +133,24 @@ 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
     addDebugItem "dump aliases" (fun _ ->
       let status = script#grafite_status in
-      LexiconEngine.dump_aliases HLog.debug "" status);
+      LexiconEngine.dump_aliases prerr_endline "" status);
 (* FG: DEBUGGING   
     addDebugItem "dump interpretations" (fun _ ->
       let status = script#lexicon_status in
@@ -191,29 +199,25 @@ 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 "tactics logging" 
+      (fun mi () -> NTacStatus.debug := mi#active);
+    addDebugCheckbox "auto logging"
+      (fun mi () -> NAuto.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);
+    addDebugCheckbox "reduction logging"
+      (fun mi () -> NCicReduction.debug := mi#active; CicReduction.ndebug := mi#active);
     addDebugSeparator ();
     addDebugItem "Expand virtuals"
     (fun _ -> (MatitaScript.current ())#expandAllVirtuals);