From 3cbfaee24c52c2e9a2070890e9f343fa06f4d0b8 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Wed, 24 Oct 2012 12:54:51 +0000
Subject: Patch by Dan Liew: "Moved PrintContext class out of ExprPrinter.cpp
 so it can be used by other classes. It has also been improved so it can be
 used with the soon to be added ExprSMTLIBPrinter classes."

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166555 91177308-0d34-0410-b5e6-96231b3b80d8
---
 include/klee/util/PrintContext.h | 91 ++++++++++++++++++++++++++++++++++++++++
 lib/Expr/ExprPPrinter.cpp        | 43 +------------------
 2 files changed, 92 insertions(+), 42 deletions(-)
 create mode 100644 include/klee/util/PrintContext.h

diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h
new file mode 100644
index 00000000..a9e91925
--- /dev/null
+++ b/include/klee/util/PrintContext.h
@@ -0,0 +1,91 @@
+#ifndef PRINTCONTEXT_H_
+#define PRINTCONTEXT_H_
+
+#include <ostream>
+#include <sstream>
+#include <string>
+#include <stack>
+#include <iomanip>
+
+/// PrintContext - Helper class for pretty printing.
+/// It provides a basic wrapper around std::ostream that keeps track of
+/// how many characters have been used on the current line.
+///
+/// It also provides an optional way keeping track of the various levels of indentation
+/// by using a stack.
+/// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
+class PrintContext {
+private:
+  std::ostream &os;
+  std::stringstream ss;
+  std::string newline;
+
+  ///This is used to keep track of the stack of indentations used by
+  /// \sa breakLineI()
+  /// \sa pushIndent()
+  /// \sa popIndent()
+  std::stack<unsigned int> indentStack;
+
+public:
+  /// Number of characters on the current line.
+  unsigned pos;
+
+  PrintContext(std::ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
+  {
+	  indentStack.push(pos);
+  }
+
+  void setNewline(const std::string &_newline) {
+    newline = _newline;
+  }
+
+  void breakLine(unsigned indent=0) {
+    os << newline;
+    if (indent)
+      os << std::setw(indent) << ' ';
+    pos = indent;
+  }
+
+  ///Break line using the indent on the top of the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& breakLineI()
+  {
+	  breakLine(indentStack.top());
+	  return *this;
+  }
+
+  ///Add the current position on the line to the top of the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& pushIndent()
+  {
+	  indentStack.push(pos);
+	  return *this;
+  }
+
+  ///Pop the top off the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& popIndent()
+  {
+	  indentStack.pop();
+	  return *this;
+  }
+
+  /// write - Output a string to the stream and update the
+  /// position. The stream should not have any newlines.
+  void write(const std::string &s) {
+    os << s;
+    pos += s.length();
+  }
+
+  template <typename T>
+  PrintContext &operator<<(T elt) {
+    ss.str("");
+    ss << elt;
+    write(ss.str());
+    return *this;
+  }
+
+};
+
+
+#endif /* PRINTCONTEXT_H_ */
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 6e7ccd2d..ac1d1d01 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -7,6 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include "klee/util/PrintContext.h"
 #include "klee/util/ExprPPrinter.h"
 
 #include "klee/Constraints.h"
@@ -38,48 +39,6 @@ namespace {
   PCAllConstWidths("pc-all-const-widths",  llvm::cl::init(false));
 }
 
-/// PrintContext - Helper class for storing extra information for
-/// the pretty printer.
-class PrintContext {
-private:
-  std::ostream &os;
-  std::stringstream ss;
-  std::string newline;
-
-public:
-  /// Number of characters on the current line.
-  unsigned pos;
-
-public:
-  PrintContext(std::ostream &_os) : os(_os), newline("\n"), pos(0) {}
-
-  void setNewline(const std::string &_newline) {
-    newline = _newline;
-  }
-
-  void breakLine(unsigned indent=0) {
-    os << newline;
-    if (indent)
-      os << std::setw(indent) << ' ';
-    pos = indent;
-  }
-
-  /// write - Output a string to the stream and update the
-  /// position. The stream should not have any newlines.
-  void write(const std::string &s) {
-    os << s;
-    pos += s.length();
-  }
-
-  template <typename T>
-  PrintContext &operator<<(T elt) {
-    ss.str("");
-    ss << elt;
-    write(ss.str());
-    return *this;
-  }
-};
-
 class PPrinter : public ExprPPrinter {
 public:
   std::set<const Array*> usedArrays;
-- 
cgit 1.4.1