From e95a0c2559c98072d9de085ff18951d557d6465a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Aug 2013 12:08:49 -0700
Subject: [PATCH] Modify basic printer for contexts

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/printer.cpp | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/library/printer.cpp b/src/library/printer.cpp
index 3f213ba738..c25f7a26a0 100644
--- a/src/library/printer.cpp
+++ b/src/library/printer.cpp
@@ -139,15 +139,22 @@ std::ostream & operator<<(std::ostream & out, std::pair<expr const &, context co
     return out;
 }
 
-std::ostream & operator<<(std::ostream & out, context const & ctx) {
+static void display_context_core(std::ostream & out, context const & ctx) {
     if (ctx) {
-        out << tail(ctx);
+        display_context_core(out, tail(ctx));
+        if (tail(ctx))
+            out << "; ";
         out << head(ctx).get_name() << " : " << head(ctx).get_domain();
         if (head(ctx).get_body()) {
             out << " := " << mk_pair(head(ctx).get_body(), tail(ctx));
         }
-        out << "\n";
     }
+}
+
+std::ostream & operator<<(std::ostream & out, context const & ctx) {
+    out << "[";
+    display_context_core(out, ctx);
+    out << "]";
     return out;
 }