diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/output.h | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/src/util/output.h b/src/util/output.h index da1efe68a..8a90ef136 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -112,19 +112,7 @@ public: operator std::ostream&() { return isConnected() ? *d_os : null_os; } template <class T> - CVC4ostream& operator<<(T const& t) { - if(d_os != NULL) { - if(d_firstColumn) { - d_firstColumn = false; - long indent = d_os->iword(s_indentIosIndex); - for(long i = 0; i < indent; ++ i) { - d_os = &(*d_os << s_tab); - } - } - d_os = &(*d_os << t); - } - return *this; - } + CVC4ostream& operator<<(T const& t) CVC4_PUBLIC; // support manipulators, endl, etc.. CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) { @@ -164,6 +152,21 @@ inline CVC4ostream& pop(CVC4ostream& stream) { return stream; } +template <class T> +CVC4ostream& CVC4ostream::operator<<(T const& t) { + if(d_os != NULL) { + if(d_firstColumn) { + d_firstColumn = false; + long indent = d_os->iword(s_indentIosIndex); + for(long i = 0; i < indent; ++i) { + d_os = &(*d_os << s_tab); + } + } + d_os = &(*d_os << t); + } + return *this; +} + /** The debug output class */ class CVC4_PUBLIC DebugC { std::set<std::string> d_tags; |