X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=11ae70642bf6b36c5f59e2b644648ca23522c7e7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=dd8d6d83dad6a115d6e13540a44fc128ca8c0cb7;hpb=6fa89cef6aa8fc1774db065a9fcfc47867579054;p=helm.git

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index dd8d6d83d..11ae70642 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -121,10 +121,6 @@ let _ =
     addDebugItem "print selections" (fun () ->
       let cicMathView = MatitaMathView.cicMathView_instance () in
       List.iter MatitaLog.debug (cicMathView#string_of_selections));
-    addDebugItem "dump getter settings" (fun _ ->
-      prerr_endline (Http_getter_env.env_to_string ()));
-    addDebugItem "getter: getalluris" (fun _ ->
-      List.iter prerr_endline (Http_getter.getalluris ()));
     addDebugItem "dump script status" script#dump;
     addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
       Helm_registry.save_to "./foo.conf.xml");
@@ -168,6 +164,15 @@ let _ =
       (fun _ ->
          let nb = gui#main#hintNotebook in
          nb#goto_page ((nb#current_page + 1) mod 3));
+    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 }}} *)