diff options
| author | Morgan Deters <mdeters@gmail.com> | 2009-12-03 14:59:30 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2009-12-03 14:59:30 +0000 |
| commit | 7fb54afe126e5045fc6c5553c1aff3c3f73509aa (patch) | |
| tree | 37f4f23af0eccd6c9615a5af9b2d219e305d1f78 /src/util/output.h | |
| parent | bde1a14afc211c8f0f0521bb91feb562eaa9f9ea (diff) | |
parsing/expr/command/result/various other fixes
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 */ |