From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 23 Aug 2008 19:10:31 +0000 (+0000)
Subject: New debug item to print aliases.
X-Git-Tag: make_still_working~4853
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f75a636a0f3d548bcf485df9b51ac72ed4759c97;p=helm.git

New debug item to print aliases.
---

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 62e425bf3..64d1a4513 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -116,6 +116,9 @@ let _ =
     let addDebugSeparator () =
       ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
     in
+    addDebugItem "dump aliases" (fun _ ->
+      let status = script#lexicon_status in
+      HLog.debug (DisambiguatePp.pp_environment status.LexiconEngine.aliases));
     addDebugItem "dump environment to \"env.dump\"" (fun _ ->
       let oc = open_out "env.dump" in
       CicEnvironment.dump_to_channel oc;