From 01736bf82afba306d8ed3772cf11fc9ef337a6fe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 23 Aug 2014 12:00:32 -0700
Subject: [PATCH] feat(util/sexpr/format): expose flatten

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/format.cpp | 8 ++++++++
 src/util/sexpr/format.cpp | 6 +++---
 src/util/sexpr/format.h   | 2 +-
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/tests/util/format.cpp b/src/tests/util/format.cpp
index 225c400c5..d098da3b7 100644
--- a/src/tests/util/format.cpp
+++ b/src/tests/util/format.cpp
@@ -120,6 +120,13 @@ static void tst5() {
     std::cout << "{" << format() << "}" << "\n";
 }
 
+static void tst6() {
+    format r = (format("test") ^ format("hello")) + line() + format("world");
+    std::cout << "test6\n";
+    std::cout << r << "\n";
+    std::cout << flatten(r) << "\n";
+}
+
 int main() {
     save_stack_info();
     tst1();
@@ -127,5 +134,6 @@ int main() {
     tst3();
     tst4();
     tst5();
+    tst6();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp
index 0fbed3efa..605734307 100644
--- a/src/util/sexpr/format.cpp
+++ b/src/util/sexpr/format.cpp
@@ -152,12 +152,12 @@ sexpr format::flatten(sexpr const & s) {
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
-format format::flatten(format const & f){
-    return format(flatten(f.m_value));
+format flatten(format const & f){
+    return format(format::flatten(f.m_value));
 }
 format group(format const & f) {
     get_g_diff_flatten() = false;
-    format flat_f = format::flatten(f);
+    format flat_f = flatten(f);
     if (get_g_diff_flatten()) {
         return choice(flat_f, f);
     } else {
diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h
index 2a18de6a1..e0d2d6366 100644
--- a/src/util/sexpr/format.h
+++ b/src/util/sexpr/format.h
@@ -41,7 +41,6 @@ public:
 private:
     sexpr m_value;
     static sexpr flatten(sexpr const & s);
-    static format flatten(format const & f);
 
     // Functions for the internal sexpr representation
     static inline format_kind sexpr_kind(sexpr const & s) {
@@ -196,6 +195,7 @@ public:
     friend format above(format const & f1, format const & f2);
     friend format bracket(std::string const & l, format const & x, std::string const & r);
     friend format wrap(format const & f1, format const & f2);
+    friend format flatten(format const & f);
 
     // x + y = x <> y
     friend format operator+(format const & f1, format const & f2);