michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/trace): register debug trace class

Browse source
This commit is contained in:
Daniel Selsam 2016-01-13 11:28:28 -08:00 committed by Leonardo de Moura
parent 599ec08c70
commit 58d41e486c
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/blast/blast.cpp
View file

@ -1380,6 +1380,7 @@ void initialize_blast() {
register_trace_class(name{"blast", "action"});
register_trace_class(name{"blast", "search"});
register_trace_class(name{"blast", "deadend"});
register_trace_class(name{"debug", "blast"});
register_trace_class_alias("app_builder", name({"blast", "event"}));
register_trace_class_alias(name({"simplifier", "failure"}), name({"blast", "event"}));

2
src/library/trace.cpp
View file

@ -186,6 +186,8 @@ io_state_stream const & operator<<(io_state_stream const & ios, tclass const & c
void initialize_trace() {
g_trace_classes = new name_set();
g_trace_aliases = new name_map<name_set>();
register_trace_class(name{"debug"});
}
void finalize_trace() {