From 4b7fe064fe4f2a4e440dfbcf4a23d2b15b94da4d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 22 Feb 2014 23:17:52 -0800
Subject: [PATCH] refactor(kernel): finish formatter interface

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/formatter.cpp   | 6 ++++++
 src/kernel/formatter.h     | 5 +----
 src/library/CMakeLists.txt | 6 +++---
 3 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp
index 213dc5cbf..909996c39 100644
--- a/src/kernel/formatter.cpp
+++ b/src/kernel/formatter.cpp
@@ -151,6 +151,12 @@ public:
     virtual format operator()(expr const & e, options const &) {
         std::ostringstream s; s << e; return format(s.str());
     }
+    virtual format operator()(object const & /* obj */, options const & /* opts */) {
+        return format(); // TODO(Leo)
+    }
+    virtual format operator()(ro_environment const & /* env */, options const & /* opts */) {
+        return format(); // TODO(Leo)
+    }
 };
 formatter mk_simple_formatter() {
     return mk_formatter(simple_formatter_cell());
diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h
index 44c9f7358..39cdf560c 100644
--- a/src/kernel/formatter.h
+++ b/src/kernel/formatter.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <memory>
 #include "util/sexpr/options.h"
+#include "kernel/environment.h"
 #include "kernel/expr.h"
 
 namespace lean {
@@ -18,7 +19,6 @@ public:
     virtual ~formatter_cell() {}
     /** \brief Format the given expression. */
     virtual format operator()(expr const & e, options const & opts) = 0;
-#if 0
     /** \brief Format the given object */
     virtual format operator()(object const & obj, options const & opts) = 0;
     /** \brief Format the given environment */
@@ -29,7 +29,6 @@ public:
         Not every formatter has an associated environment object.
     */
     virtual optional<ro_environment> get_environment() const { return optional<ro_environment>(); }
-#endif
 };
 /**
    \brief Smart-pointer for the actual formatter object (aka \c formatter_cell).
@@ -39,11 +38,9 @@ class formatter {
     formatter(formatter_cell * c):m_cell(c) {}
 public:
     format operator()(expr const & e, options const & opts = options()) const { return (*m_cell)(e, opts); }
-#if 0
     format operator()(object const & obj, options const & opts = options()) const { return (*m_cell)(obj, opts); }
     format operator()(ro_environment const & env, options const & opts = options()) const { return (*m_cell)(env, opts); }
     optional<ro_environment> get_environment() { return m_cell->get_environment(); }
-#endif
     template<typename FCell> friend formatter mk_formatter(FCell && fcell);
 };
 
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 341a34c9e..4161d4629 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,7 +1,7 @@
-add_library(library deep_copy.cpp expr_lt.cpp)
+add_library(library deep_copy.cpp expr_lt.cpp io_state_stream.cpp)
 # kernel_bindings.cpp
-# context_to_lambda.cpp placeholder.cpp  substitution.cpp
-# fo_unify.cpp bin_op.cpp equality.cpp io_state_stream.cpp printer.cpp
+# context_to_lambda.cpp placeholder.cpp
+# fo_unify.cpp bin_op.cpp equality.cpp printer.cpp
 # hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})