From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 18 Nov 2005 16:52:13 +0000 (+0000)
Subject: added debug items for enabling/disabling pretty printing notation completely
X-Git-Tag: V_0_7_2_3~36
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=af364f229a858464cc557e60e314b6ffb20b6625

added debug items for enabling/disabling pretty printing notation completely
---

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index da09fb27d..11ae70642 100644
--- 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 }}} *)