From 1038f7346ee76dd60840a7b6289f67b6a7fbe315 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Aug 2013 09:30:08 -0700
Subject: [PATCH] Refine initialization order. Polish Universe command pretty
 printer.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontend/frontend.cpp       | 4 ++--
 src/kernel/environment.cpp      | 2 +-
 src/tests/frontend/frontend.cpp | 3 +--
 3 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp
index d722e8b55..749cc7cfe 100644
--- a/src/frontend/frontend.cpp
+++ b/src/frontend/frontend.cpp
@@ -195,8 +195,7 @@ struct frontend::imp {
     void add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixc(sz, opns, p), n, false); }
 
     imp(frontend & fe):
-        m_num_children(0),
-        m_env(mk_toplevel()) {
+        m_num_children(0) {
     }
 
     explicit imp(std::shared_ptr<imp> const & parent):
@@ -214,6 +213,7 @@ struct frontend::imp {
 
 frontend::frontend():m_imp(new imp(*this)) {
     init_builtin_notation(*this);
+    init_toplevel(m_imp->m_env);
     m_imp->m_env.set_formatter(mk_pp_expr_formatter(*this, options()));
 }
 frontend::frontend(imp * new_ptr):m_imp(new_ptr) {}
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 6b0735cc3..57e523e9a 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -29,7 +29,7 @@ public:
     static char const * g_keyword;
     virtual char const * keyword() const { return g_keyword; }
     virtual format pp(environment const &) const {
-        return format{format(keyword()), space(), format(m_name), space(), format("\u2265"), space(), ::lean::pp(m_level)};
+        return format{highlight_command(format(keyword())), space(), format(m_name), space(), format("\u2265"), space(), ::lean::pp(m_level)};
     }
 };
 char const * uvar_declaration::g_keyword = "Universe";
diff --git a/src/tests/frontend/frontend.cpp b/src/tests/frontend/frontend.cpp
index 2f5e7abc1..3048b2e7c 100644
--- a/src/tests/frontend/frontend.cpp
+++ b/src/tests/frontend/frontend.cpp
@@ -48,8 +48,7 @@ static void tst2() {
 
 static void tst3() {
     frontend f;
-    f.add_infixl("+", 10, name{"Int", "add"});
-    f.add_infixl("-", 10, name{"Int", "sub"});
+    std::cout << "====================\n";
     std::cout << f;
 }