push and pop manipulators for output stream so that one can indent the output

ueful for me, maybe someone else finds it useful also

diff --git a/src/util/output.h b/src/util/output.h
index d722b10d1d16f42cfc7892ab4a455148716853f5..dd5007747f714b0e3ccad0f424df4cae099e0f1e 100644 (file)
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -134,9 +134,19 @@ extern NullC nullCvc4Stream CVC4_PUBLIC;
 
 class CVC4_PUBLIC CVC4ostream {
   std::ostream* d_os;
+  // Current indentation
+  unsigned d_indent;
+
+  std::ostream& (*d_endl)(std::ostream&);
+
 public:
   CVC4ostream() : d_os(NULL) {}
-  CVC4ostream(std::ostream* os) : d_os(os) {}
+  CVC4ostream(std::ostream* os) : d_os(os), d_indent(0) {
+    d_endl = &std::endl;
+  }
+
+  void pushIndent() { d_indent ++; };
+  void popIndent()  { if (d_indent > 0) -- d_indent; }
 
   void flush() {
     if(d_os != NULL) {
@@ -160,6 +170,11 @@ public:
     if(d_os != NULL) {
       d_os = &(*d_os << pf);
     }
+    if (pf == d_endl) {
+      for (unsigned i = 0; i < d_indent; ++ i) {
+        d_os = &(*d_os << '\t');
+      }
+    }
     return *this;
   }
   CVC4ostream& operator<<(std::ios& (*pf)(std::ios&)) {
@@ -174,9 +189,23 @@ public:
     }
     return *this;
   }
-
+  CVC4ostream& operator<<(CVC4ostream& (*pf)(CVC4ostream&)) {
+    return pf(*this);
+  }
 };/* class CVC4ostream */
 
+inline CVC4ostream& push(CVC4ostream& stream)
+{
+  stream.pushIndent();
+  return stream;
+}
+
+inline CVC4ostream& pop(CVC4ostream& stream)
+{
+  stream.popIndent();
+  return stream;
+}
+
 /** The debug output class */
 class CVC4_PUBLIC DebugC {
   std::set<std::string> d_tags;