From efbf3a434d56acbaeeffed430bea84a272cca03b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Aug 2013 20:00:12 -0700 Subject: [PATCH] Highlight assignment keyword Signed-off-by: Leonardo de Moura --- src/frontend/pp.cpp | 2 +- src/kernel/expr_formatter.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontend/pp.cpp b/src/frontend/pp.cpp index 250d575d2..a281e75aa 100644 --- a/src/frontend/pp.cpp +++ b/src/frontend/pp.cpp @@ -403,7 +403,7 @@ struct pp_fn { format body_sep; if (B) { format B_f = pp(B, 0).first; - body_sep = format{space(), colon(), space(), B_f, space(), format(":=")}; + body_sep = format{space(), colon(), space(), B_f, space(), highlight_keyword(format(":="))}; } else { body_sep = comma(); } diff --git a/src/kernel/expr_formatter.cpp b/src/kernel/expr_formatter.cpp index c257c22fc..fba1d8bcc 100644 --- a/src/kernel/expr_formatter.cpp +++ b/src/kernel/expr_formatter.cpp @@ -11,7 +11,7 @@ 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)}; + operator()(t), space(), highlight_keyword(format(":=")), line(), operator()(v)}; return group(nest(def)); }