moved initial (i.e. empty) lexiconEngine status to lexiconEngine from

[helm.git] / matita / matita.ml

diff --git a/matita/matita.ml b/matita/matita.ml
index 07f7f900ae9c1f727b97b797b3eab362445ed165..a8a031273b309a05f7316449d4ed57e46c8d1f24 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -141,6 +141,17 @@ let _ =
             (UriManager.name_of_uri u ^ ":"
              ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
         (CoercDb.to_list ()));
+    addDebugItem "show coercions graph" (fun _ ->
+      let str = CoercGraph.generate_dot_file () in
+      let filename, oc = Filename.open_temp_file "xx" ".dot" in
+      output_string oc str;
+      close_out oc;
+      let ps = Filename.temp_file "yy" ".png" in
+      ignore (Unix.system ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename));
+      ignore (Unix.system ("/usr/bin/display " ^ ps));
+      Sys.remove ps;
+      Sys.remove filename);
+        
     addDebugItem "print top-level grammar entries"
       CicNotationParser.print_l2_pattern;
     addDebugItem "dump moo to stderr" (fun _ ->
@@ -180,6 +191,10 @@ let _ =
       (fun _ ->
         CicNotation.set_active_notations
           (List.map fst (CicNotation.get_all_notations ())));
+    addDebugItem "enable coercions hiding"
+      (fun _ -> TermAcicContent.hide_coercions := true);
+    addDebugItem "disable coercions hiding"
+      (fun _ -> TermAcicContent.hide_coercions := false);
   end
   (** Debugging }}} *)