From ef18cc4a922089fb7661ef88b42ddeea3eea0159 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Dec 2013 13:38:14 -0800
Subject: [PATCH] fix(frontends/lean/parser): add existing command macros when
 creating parser object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp       | 11 +++++++----
 tests/lean/nested.lean              | 20 ++++++++++++++++++++
 tests/lean/nested.lean.expected.out |  5 +++++
 3 files changed, 32 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/nested.lean
 create mode 100644 tests/lean/nested.lean.expected.out

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index aea843cca..9b53a59fe 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2546,19 +2546,22 @@ public:
         m_script_state(S),
         m_set_parser(m_script_state, this) {
         m_check_identifiers = true;
+        updt_options();
+        m_found_errors = false;
+        m_num_local_decls = 0;
+        m_scanner.set_command_keywords(g_command_keywords);
         if (m_script_state) {
             m_script_state->apply([&](lua_State * L) {
                     m_expr_macros = &get_expr_macros(L);
                     m_cmd_macros  = &get_cmd_macros(L);
+                    for (auto const & p : *m_cmd_macros) {
+                        m_scanner.add_command_keyword(p.first);
+                    }
                 });
         } else {
             m_expr_macros = nullptr;
             m_cmd_macros  = nullptr;
         }
-        updt_options();
-        m_found_errors = false;
-        m_num_local_decls = 0;
-        m_scanner.set_command_keywords(g_command_keywords);
         scan();
     }
 
diff --git a/tests/lean/nested.lean b/tests/lean/nested.lean
new file mode 100644
index 000000000..580621243
--- /dev/null
+++ b/tests/lean/nested.lean
@@ -0,0 +1,20 @@
+(**
+cmd_macro("Simple",
+          { macro_arg.String },
+          function (env, str)
+             print("OUTPUT: " .. str)
+          end
+)
+
+parse_lean_cmds([[
+   Simple "foo"
+]])
+**)
+
+Simple "testing"
+
+(**
+parse_lean_cmds([[
+   Simple "bla"
+]])
+**)
diff --git a/tests/lean/nested.lean.expected.out b/tests/lean/nested.lean.expected.out
new file mode 100644
index 000000000..30d4c78dd
--- /dev/null
+++ b/tests/lean/nested.lean.expected.out
@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+OUTPUT: foo
+OUTPUT: testing
+OUTPUT: bla