diff options
Diffstat (limited to 'src/util/output.h')
| -rw-r--r-- | src/util/output.h | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/util/output.h b/src/util/output.h index 4d3752849..21b7b6e4c 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -20,7 +20,6 @@ namespace CVC4 { - class Debug { std::set<std::string> d_tags; std::ostream &d_out; @@ -30,19 +29,23 @@ public: static void operator()(const char* tag, std::string); static void operator()(string tag, const char*); static void operator()(string tag, std::string); + static void operator()(const char*);// Yeting option + static void operator()(std::string);// Yeting option static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + // Yeting option not possible here static std::ostream& operator()(const char* tag); static std::ostream& operator()(std::string tag); + static std::ostream& operator()();// Yeting option - static void on (const char* tag) { d_tags.insert(std::string(tag)); }; - static void on (std::string tag) { d_tags.insert(tag); }; - static void off(const char* tag) { d_tags.erase (std::string(tag)); }; - static void off(std::string tag) { d_tags.erase (tag); }; + static void on (const char* tag) { d_tags.insert(std::string(tag)); } + static void on (std::string tag) { d_tags.insert(tag); } + static void off(const char* tag) { d_tags.erase (std::string(tag)); } + static void off(std::string tag) { d_tags.erase (tag); } static void setStream(std::ostream& os) { d_out = os; } };/* class Debug */ |