From 5ec278032117ab52ddc9a5b77a0ae24079726a18 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Aug 2013 19:26:49 -0700
Subject: [PATCH] Extend formatter with support for definitions and postulates.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/expr_formatter.cpp | 12 ++++++++++++
 src/kernel/expr_formatter.h   |  5 +++++
 src/kernel/object.cpp         |  7 ++-----
 3 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/src/kernel/expr_formatter.cpp b/src/kernel/expr_formatter.cpp
index cd5f05a9d..c257c22fc 100644
--- a/src/kernel/expr_formatter.cpp
+++ b/src/kernel/expr_formatter.cpp
@@ -8,6 +8,18 @@ Author: Leonardo de Moura
 #include "exception.h"
 
 namespace lean {
+
+format expr_formatter::operator()(char const * kwd, name const & n, expr const & t, expr const & v) {
+    format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(),
+                        operator()(t), format(" :="), line(), operator()(v)};
+    return group(nest(def));
+}
+
+format expr_formatter::operator()(char const * kwd, name const & n, expr const & t) {
+    format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), operator()(t)};
+    return group(nest(def));
+}
+
 void expr_formatter::pp(std::ostream & out, expr const & e, context const & c) {
     out << mk_pair(operator()(e, c), get_options());
 }
diff --git a/src/kernel/expr_formatter.h b/src/kernel/expr_formatter.h
index c075cf602..51806ca74 100644
--- a/src/kernel/expr_formatter.h
+++ b/src/kernel/expr_formatter.h
@@ -16,6 +16,11 @@ public:
     virtual ~expr_formatter() {}
     /** \brief Convert expression in the given context into a format object. */
     virtual format operator()(expr const & e, context const & c = context()) = 0;
+    /** \brief format a definition. */
+    virtual format operator()(char const * kwd, name const & n, expr const & t, expr const & v);
+    /** \brief format a postulate. */
+    virtual format operator()(char const * kwd, name const & n, expr const & t);
+
     /** \brief Return options for pretty printing. */
     virtual options get_options() const = 0;
 
diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp
index 18df9c48e..24049e681 100644
--- a/src/kernel/object.cpp
+++ b/src/kernel/object.cpp
@@ -36,9 +36,7 @@ bool         definition::is_opaque() const     { return m_opaque; }
 expr const & definition::get_value() const     { return m_value; }
 format       definition::pp(environment const & env) const {
     expr_formatter & fmt = env.get_formatter();
-    format def = format{highlight_command(format(keyword())), space(), format(get_name()), space(), colon(), space(),
-                        fmt(get_type()), format(" :="), line(), fmt(get_value())};
-    return group(fmt.nest(def));
+    return fmt(keyword(), get_name(), get_type(), get_value());
 }
 
 char const * theorem::g_keyword = "Theorem";
@@ -53,8 +51,7 @@ bool         fact::is_opaque() const     { lean_unreachable(); return false; }
 expr const & fact::get_value() const     { lean_unreachable(); return expr::null(); }
 format fact::pp(environment const & env) const {
     expr_formatter & fmt = env.get_formatter();
-    format def = format{highlight_command(format(keyword())), space(), format(get_name()), space(), colon(), space(), fmt(get_type())};
-    return group(fmt.nest(def));
+    return fmt(keyword(), get_name(), get_type());
 }
 
 char const * axiom::g_keyword = "Axiom";