added debug items for enabling/disabling pretty printing notation completely

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index da09fb27dbea99945d407ad9003bdf7e64efccd3..11ae70642bf6b36c5f59e2b644648ca23522c7e7 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -167,6 +167,12 @@ let _ =
     addDebugItem "print runtime dir"
       (fun _ ->
         prerr_endline BuildTimeConf.runtime_base_dir);
+    addDebugItem "disable all (pretty printing) notations"
+      (fun _ -> CicNotation.set_active_notations []);
+    addDebugItem "enable all (pretty printing) notations"
+      (fun _ ->
+        CicNotation.set_active_notations
+          (List.map fst (CicNotation.get_all_notations ())));
   end
   (** Debugging }}} *)