From 5f10d470350ae73dd34c624c2be624bf2a4bdaef Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Fri, 2 Aug 2013 19:17:29 -0700
Subject: [PATCH] Change operators in format: f1 + f2 = f1 <> f2 f1 ^ f2 = f1
 <> " " <> f2

---
 src/util/format.cpp |  4 ++++
 src/util/format.h   | 13 +++++++++++--
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/util/format.cpp b/src/util/format.cpp
index d2c8bfd37..9c3be77da 100644
--- a/src/util/format.cpp
+++ b/src/util/format.cpp
@@ -237,6 +237,10 @@ format operator+(format const & f1, format const & f2) {
     return format{f1, f2};
 }
 
+format operator^(format const & f1, format const & f2) {
+    return format{f1, format(" "), f2};
+}
+
 std::ostream & pretty(std::ostream & out, unsigned w, format const & f) {
     sexpr const & b = format::best(w, 0, f.m_value);
     return layout_list(out, b);
diff --git a/src/util/format.h b/src/util/format.h
index 6d26319f3..8520600bc 100644
--- a/src/util/format.h
+++ b/src/util/format.h
@@ -177,13 +177,22 @@ public:
     friend format bracket(std::string const l, format const & x, std::string const r);
     friend format wrap(format const & f1, format const & f2);
 
+    // x + y = x <> y
+    friend format operator+(format const & f1, format const & f2);
     format & operator+=(format const & f) {
         *this = *this + f;
         return *this;
     }
+
+    // x ^ y = x <> " " <> y
+    friend format operator^(format const & f1, format const & f2);
+    format & operator^=(format const & f) {
+        *this = *this ^ f;
+        return *this;
+    }
+
     friend std::ostream & operator<<(std::ostream & out, format const & f);
-    // x <+> y = x <> text " " <> y
-    friend format operator+(format const & f1, format const & f2);
+
     friend std::ostream & layout(std::ostream & out, sexpr const & s);
     friend std::ostream & pretty(std::ostream & out, unsigned w, format const & f);
 };