From 577256fedc3ff5c3ad94801e7ad0e7fc1b64ba87 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Aug 2013 08:32:13 -0700
Subject: [PATCH] Add highlight_keyword, highlight_builtin, highlight_command
 for consistent formatting

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

diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp
index 2f31512ac..c9a2ce1ed 100644
--- a/src/kernel/object.cpp
+++ b/src/kernel/object.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 // TODO: delete hardcoded
-format pp_object_kind(char const * n) { return highlight(format(n), format::format_color::BLUE); }
+format pp_object_kind(char const * n) { return highlight_command(format(n)); }
 constexpr unsigned indentation = 2; // TODO: must be option
 //
 
diff --git a/src/kernel/pp.cpp b/src/kernel/pp.cpp
index fc68e6212..6af9498ed 100644
--- a/src/kernel/pp.cpp
+++ b/src/kernel/pp.cpp
@@ -17,9 +17,9 @@ struct pp_fn {
     pp_fn(environment const * env):m_env(env) {}
 
     unsigned indent() const { return 2; }
-    format pp_keyword(char const * k) { return highlight(format(k), format::format_color::ORANGE); }
-    format pp_type_kwd() { return highlight(format("Type"), format::format_color::PINK); }
-    format pp_eq_kwd() { return highlight(format(" = "), format::format_color::BLUE); }
+    format pp_keyword(char const * k) { return highlight_keyword(format(k)); }
+    format pp_type_kwd() { return highlight_builtin(format("Type")); }
+    format pp_eq_kwd() { return format(" = "); }
     format pp_lambda_kwd() { return pp_keyword("\u03BB "); }
     format pp_lambda_sep() { return format(","); }
     format pp_pi_kwd() { return pp_keyword("\u03A0 "); }
diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp
index d0ddd8c23..2deac2474 100644
--- a/src/util/sexpr/format.cpp
+++ b/src/util/sexpr/format.cpp
@@ -23,6 +23,18 @@
 #define LEAN_DEFAULT_PP_COLORS true
 #endif
 
+#ifndef LEAN_KEYWORD_HIGHLIGHT_COLOR
+#define LEAN_KEYWORD_HIGHLIGHT_COLOR format::ORANGE
+#endif
+
+#ifndef LEAN_BUILTIN_HIGHLIGHT_COLOR
+#define LEAN_BUILTIN_HIGHLIGHT_COLOR format::CYAN
+#endif
+
+#ifndef LEAN_COMMAND_HIGHLIGHT_COLOR
+#define LEAN_COMMAND_HIGHLIGHT_COLOR format::BLUE
+#endif
+
 namespace lean {
 static name g_pp_indent{"pp", "indent"};
 static name g_pp_colors{"pp", "colors"};
@@ -99,6 +111,15 @@ format nest(int i, format const & f) {
 format highlight(format const & f, format::format_color const c) {
     return format(format::sexpr_highlight(f.m_value, c));
 }
+format highlight_keyword(format const & f) {
+    return highlight(f, LEAN_KEYWORD_HIGHLIGHT_COLOR);
+}
+format highlight_builtin(format const & f) {
+    return highlight(f, LEAN_BUILTIN_HIGHLIGHT_COLOR);
+}
+format highlight_command(format const & f) {
+    return highlight(f, LEAN_COMMAND_HIGHLIGHT_COLOR);
+}
 // Commonly used format objects
 format mk_line() {
     return format(format::sexpr_line());
diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h
index 2f3b3005d..d42e86d70 100644
--- a/src/util/sexpr/format.h
+++ b/src/util/sexpr/format.h
@@ -214,6 +214,9 @@ format wrap(format const & f1, format const & f2);
 format compose(format const & f1, format const & f2);
 format nest(int i, format const & f);
 format highlight(format const & f, format::format_color const c);
+format highlight_keyword(format const & f);
+format highlight_builtin(format const & f);
+format highlight_command(format const & f);
 format const & line();
 format const & space();
 format const & lp();