From 4d6cbf79c1202f541c3a63af05fd426427b94423 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 13 Sep 2005 13:24:22 +0000 Subject: [PATCH] added moo dumping debug item --- helm/matita/matita.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index b9019a035..6e5af0645 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -149,6 +149,10 @@ let _ = (CoercDb.to_list ())); addDebugItem "print top-level grammar entries" CicNotationParser.print_l2_pattern; + addDebugItem "dump moo to stderr" (fun _ -> + let status = (MatitaScript.instance ())#status in + List.iter (fun cmd -> prerr_endline + (GrafiteAstPp.pp_command cmd)) (List.rev status.moo_content_rev)); addDebugItem "rotate light bulbs" (fun _ -> let nb = gui#main#hintNotebook in -- 2.39.2