From 9d1cd073c57a1fa3b99961dee1e2a86d3363faff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Feb 2015 10:12:45 -0800
Subject: [PATCH] feat(frontends/lean): add 'print metaclasses' command

---
 src/frontends/lean/builtin_cmds.cpp | 10 ++++++++++
 src/frontends/lean/tokens.cpp       |  4 ++++
 src/frontends/lean/tokens.h         |  1 +
 tests/lean/run/meta.lean            |  1 +
 4 files changed, 16 insertions(+)
 create mode 100644 tests/lean/run/meta.lean

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index cc1d8a455f..cacbfbfe46 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -156,6 +156,13 @@ static void print_notation(parser & p) {
         p.regular_stream() << "no notation" << endl;
 }
 
+static void print_metaclasses(parser & p) {
+    buffer<name> c;
+    get_metaclasses(c);
+    for (name const & n : c)
+        p.regular_stream() << "[" << n << "]" << endl;
+}
+
 environment print_cmd(parser & p) {
     flycheck_information info(p.regular_stream());
     if (info.enabled()) {
@@ -212,6 +219,9 @@ environment print_cmd(parser & p) {
         if (p.curr_is_identifier())
             C = p.check_constant_next("invalid 'print coercions', constant expected");
         print_coercions(p, C);
+    } else if (p.curr_is_token_or_id(get_metaclasses_tk())) {
+        p.next();
+        print_metaclasses(p);
     } else if (p.curr_is_token_or_id(get_axioms_tk())) {
         p.next();
         print_axioms(p);
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index cdcbdf0b22..4a999d2474 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -122,6 +122,7 @@ static name * g_persistent   = nullptr;
 static name * g_root         = nullptr;
 static name * g_fields       = nullptr;
 static name * g_trust        = nullptr;
+static name * g_metaclasses  = nullptr;
 
 void initialize_tokens() {
     g_period       = new name(".");
@@ -239,9 +240,11 @@ void initialize_tokens() {
     g_root         = new name("_root_");
     g_fields       = new name("fields");
     g_trust        = new name("trust");
+    g_metaclasses  = new name("metaclasses");
 }
 
 void finalize_tokens() {
+    delete g_metaclasses;
     delete g_persistent;
     delete g_root;
     delete g_fields;
@@ -359,6 +362,7 @@ void finalize_tokens() {
     delete g_period;
 }
 
+name const & get_metaclasses_tk() { return *g_metaclasses; }
 name const & get_period_tk() { return *g_period; }
 name const & get_placeholder_tk() { return *g_placeholder; }
 name const & get_colon_tk() { return *g_colon; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 1803bb243e..6dd0dbed6c 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -124,4 +124,5 @@ name const & get_persistent_tk();
 name const & get_root_tk();
 name const & get_fields_tk();
 name const & get_trust_tk();
+name const & get_metaclasses_tk();
 }
diff --git a/tests/lean/run/meta.lean b/tests/lean/run/meta.lean
new file mode 100644
index 0000000000..271169b240
--- /dev/null
+++ b/tests/lean/run/meta.lean
@@ -0,0 +1 @@
+print metaclasses