diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 8b33cd1d14..cb40936aa9 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -412,17 +412,6 @@ struct args {
 expr copy(expr const & e);
 // =======================================
 
-// =======================================
-// Expression formatter
-class expr_formatter {
-public:
-    virtual ~expr_formatter() {}
-    virtual format operator()(expr const & e) = 0;
-    virtual options const & get_options() const = 0;
-};
-// =======================================
-
-
 // =======================================
 // Update
 template<typename F> expr update_app(expr const & e, F f) {
diff --git a/src/tests/util/format.cpp b/src/tests/util/format.cpp
index 4e4e1533f5..4dc793d116 100644
--- a/src/tests/util/format.cpp
+++ b/src/tests/util/format.cpp
@@ -9,7 +9,7 @@ Author: Soonho Kong
 #include "format.h"
 #include "test.h"
 #include "sexpr_funcs.h"
-
+#include "options.h"
 using namespace lean;
 
 using std::cout;
@@ -82,8 +82,6 @@ static void tst1() {
     pretty(cout, 60, spread(sl.begin(), sl.end()));
     cout << endl;
     cout << std::string(40, '=') << endl;
-
-    return;
 }
 
 static void tst2() {
@@ -92,9 +90,18 @@ static void tst2() {
     cout << paren(f4) << "\n";
 }
 
+static void tst3() {
+    format f_atom1("foo");
+    format f_atom2("bar");
+    format f1(highlight(f_atom1), f_atom2);
+    cout << f1 << "\n";
+    cout << mk_pair(f1, options({"pp", "colors"}, false)) << "\n";
+}
+
 int main() {
     continue_on_violation(true);
     tst1();
     tst2();
+    tst3();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/util/sexpr.cpp b/src/tests/util/sexpr.cpp
index 74e63d1af6..c20736c008 100644
--- a/src/tests/util/sexpr.cpp
+++ b/src/tests/util/sexpr.cpp
@@ -168,6 +168,10 @@ static void tst7() {
     sexpr s = sexpr{ sexpr(1,2), sexpr(2,3), sexpr(0,1) };
     std::cout << pp(sexpr{s, s, s, s, s}) << "\n";
     std::cout << pp(sexpr{sexpr(name{"test","name"}), sexpr(10), sexpr(10.20)}) << "\n";
+    format f = highlight(pp(sexpr{s, s, s, s, s}));
+    std::cout << f << "\n";
+    std::cout << mk_pair(f, options({"pp", "width"}, 1000)) << "\n";
+    std::cout << mk_pair(f, update(options({"pp", "width"}, 1000), {"pp", "colors"}, false)) << "\n";
 }
 
 int main() {
diff --git a/src/util/pair.h b/src/util/pair.h
new file mode 100644
index 0000000000..ccf1fb2a34
--- /dev/null
+++ b/src/util/pair.h
@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <utility>
+
+namespace lean {
+/** \brief Alias for make_pair */
+template<typename T1, typename T2>
+inline std::pair<T1, T2> mk_pair(T1 const & v1, T2 const & v2) {
+    return std::make_pair(v1, v2);
+}
+}
diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp
index 90d7bfa68f..966898b24e 100644
--- a/src/util/sexpr/format.cpp
+++ b/src/util/sexpr/format.cpp
@@ -11,17 +11,36 @@
 #include "sexpr_funcs.h"
 #include "options.h"
 
-#ifndef LEAN_DEFAULT_INDENTATION
-#define LEAN_DEFAULT_INDENTATION 4
+#ifndef LEAN_DEFAULT_PP_INDENTATION
+#define LEAN_DEFAULT_PP_INDENTATION 4
 #endif
 
-#ifndef LEAN_DEFAULT_WIDTH
-#define LEAN_DEFAULT_WIDTH 120
+#ifndef LEAN_DEFAULT_PP_WIDTH
+#define LEAN_DEFAULT_PP_WIDTH 120
+#endif
+
+#ifndef LEAN_DEFAULT_PP_COLORS
+#define LEAN_DEFAULT_PP_COLORS true
 #endif
 
 namespace lean {
-static int default_width = LEAN_DEFAULT_WIDTH;
-std::ostream & layout(std::ostream & out, sexpr const & s) {
+static name g_pp_indent{"pp", "indent"};
+static name g_pp_colors{"pp", "colors"};
+static name g_pp_width{"pp", "width"};
+
+unsigned get_pp_indent(options const & o) {
+    return o.get_int(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION);
+}
+
+bool get_pp_colors(options const & o) {
+    return o.get_bool(g_pp_colors, LEAN_DEFAULT_PP_COLORS);
+}
+
+unsigned get_pp_width(options const & o) {
+    return o.get_int(g_pp_width, LEAN_DEFAULT_PP_WIDTH);
+}
+
+std::ostream & layout(std::ostream & out, bool colors, sexpr const & s) {
     lean_assert(!is_nil(s));
     switch (format::sexpr_kind(s)) {
     case format::format_kind::NEST:
@@ -50,22 +69,23 @@ std::ostream & layout(std::ostream & out, sexpr const & s) {
     }
 
     case format::format_kind::COLOR_BEGIN:
-    {
-        format::format_color c = static_cast<format::format_color>(to_int(cdr(s)));
-        out << "\e[" << (31 + c % 7) << "m";
+        if (colors) {
+            format::format_color c = static_cast<format::format_color>(to_int(cdr(s)));
+            out << "\e[" << (31 + c % 7) << "m";
+        }
         break;
-    }
-
     case format::format_kind::COLOR_END:
-        out << "\e[0m";
+        if (colors) {
+            out << "\e[0m";
+        }
         break;
     }
     return out;
 }
 
-std::ostream & layout_list(std::ostream & out, sexpr const & s) {
-    for_each(s, [&out](sexpr const & s) {
-            layout(out, s);
+std::ostream & layout_list(std::ostream & out, bool colors, sexpr const & s) {
+    for_each(s, [&](sexpr const & s) {
+            layout(out, colors, s);
         });
     return out;
 }
@@ -279,10 +299,6 @@ sexpr format::best(unsigned w, unsigned k, sexpr const & s) {
     return be(w, k, sexpr{sexpr(0, s)});
 }
 
-std::ostream & operator<<(std::ostream & out, format const & f) {
-    return pretty(out, default_width, f);
-}
-
 format operator+(format const & f1, format const & f2) {
     return format{f1, f2};
 }
@@ -291,15 +307,25 @@ format operator^(format const & f1, format const & f2) {
     return format{f1, format(" "), f2};
 }
 
-std::ostream & pretty(std::ostream & out, unsigned w, format const & f) {
+std::ostream & pretty(std::ostream & out, unsigned w, bool colors, format const & f) {
     sexpr const & b = format::best(w, 0, f.m_value);
-    return layout_list(out, b);
+    return layout_list(out, colors, b);
 }
 
-static name g_pp_indent{"pp", "indent"};
+std::ostream & pretty(std::ostream & out, unsigned w, format const & f) {
+    return pretty(out, w, LEAN_DEFAULT_PP_COLORS, f);
+}
 
-unsigned get_pp_indent(options const & o) {
-    return o.get_int(g_pp_indent, LEAN_DEFAULT_INDENTATION);
+std::ostream & pretty(std::ostream & out, options const & opts, format const & f) {
+    return pretty(out, get_pp_width(opts), get_pp_colors(opts), f);
+}
+
+std::ostream & operator<<(std::ostream & out, format const & f) {
+    return pretty(out, LEAN_DEFAULT_PP_WIDTH, LEAN_DEFAULT_PP_COLORS, f);
+}
+
+std::ostream & operator<<(std::ostream & out, std::pair<format const &, options const &> const & p) {
+    return pretty(out, p.second, p.first);
 }
 
 format pp(name const & n) {
diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h
index eba21c0695..6ec48f97f0 100644
--- a/src/util/sexpr/format.h
+++ b/src/util/sexpr/format.h
@@ -12,8 +12,10 @@ Author: Soonho Kong
 #include <numeric>
 #include <sstream>
 #include "mpz.h"
+#include "pair.h"
 
 namespace lean {
+class options;
 /**
    \brief Format
 
@@ -199,10 +201,13 @@ public:
         return *this;
     }
 
-    friend std::ostream & operator<<(std::ostream & out, format const & f);
-
-    friend std::ostream & layout(std::ostream & out, sexpr const & s);
+    friend std::ostream & layout(std::ostream & out, bool colors, sexpr const & s);
+    friend std::ostream & pretty(std::ostream & out, unsigned w, bool colors, format const & f);
     friend std::ostream & pretty(std::ostream & out, unsigned w, format const & f);
+    friend std::ostream & pretty(std::ostream & out, options const & o, format const & f);
+
+    friend std::ostream & operator<<(std::ostream & out, format const & f);
+    friend std::ostream & operator<<(std::ostream & out, std::pair<format const &, options const &> const & p);
 };
 
 format wrap(format const & f1, format const & f2);
diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h
index a9f428816d..847bf619d1 100644
--- a/src/util/sexpr/options.h
+++ b/src/util/sexpr/options.h
@@ -50,5 +50,4 @@ public:
     friend std::ostream & operator<<(std::ostream & out, options const & o);
 };
 template<typename T> options update(options const & o, name const & n, T const & v) { return o.update(n, sexpr(v)); }
-template<typename T> options update(options const & o, char const * n, T const & v) { return o.update(name(n), sexpr(v)); }
 }