diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-05-09 21:52:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-05-09 21:52:38 +0000 |
commit | 6a4af721d1dc55f1dc6454014c08f87465398a54 (patch) | |
tree | 178f006869c0c4af6b6c71f46b55c28de643c7bd /src/util/output.h | |
parent | 1ce0650dcf8ce30424b546deb540974cc510c215 (diff) |
--disable-tracing at configure time now disables Trace() and Debug() gestures both.
Diffstat (limited to 'src/util/output.h')
-rw-r--r-- | src/util/output.h | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/util/output.h b/src/util/output.h index 308cfcac2..602fb69cb 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -430,13 +430,13 @@ inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; } #else /* CVC4_MUZZLE */ -# ifdef CVC4_DEBUG +# if defined(CVC4_DEBUG) && defined(CVC4_TRACING) # define Debug ::CVC4::DebugChannel -# else /* CVC4_DEBUG */ +# else /* CVC4_DEBUG && CVC4_TRACING */ # define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; } inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; } -# endif /* CVC4_DEBUG */ +# endif /* CVC4_DEBUG && CVC4_TRACING */ # define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel # define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel # define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel @@ -472,7 +472,7 @@ public: inline operator bool() { return true; } };/* __cvc4_true */ -#ifdef CVC4_DEBUG +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) class CVC4_PUBLIC ScopedDebug { std::string d_tag; @@ -509,7 +509,7 @@ public: } };/* class ScopedDebug */ -#else /* CVC4_DEBUG */ +#else /* CVC4_DEBUG && CVC4_TRACING */ class CVC4_PUBLIC ScopedDebug { public: @@ -517,7 +517,7 @@ public: ScopedDebug(const char* tag, bool newSetting = true) {} };/* class ScopedDebug */ -#endif /* CVC4_DEBUG */ +#endif /* CVC4_DEBUG && CVC4_TRACING */ #ifdef CVC4_TRACING @@ -579,13 +579,13 @@ public: inline ~IndentedScope(); };/* class IndentedScope */ -#ifdef CVC4_DEBUG +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; } inline IndentedScope::~IndentedScope() { d_out << pop; } -#else /* CVC4_DEBUG */ +#else /* CVC4_DEBUG && CVC4_TRACING */ inline IndentedScope::IndentedScope(CVC4ostream out) {} inline IndentedScope::~IndentedScope() {} -#endif /* CVC4_DEBUG */ +#endif /* CVC4_DEBUG && CVC4_TRACING */ }/* CVC4 namespace */ |