From c730dd787294536a2178ac21ecdfb61006b2f778 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Dec 2013 01:07:27 -0800
Subject: [PATCH] feat(frontends/lean/parser): propagate position information
 to expressions created by macro implemented in Lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 2e6ad9de3..b5a1a477a 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -848,6 +848,17 @@ class parser::imp {
         }
     }
 
+    void propagage_position(expr const & e, pos_info p) {
+        for_each(e, [&](expr const & e, unsigned) {
+                if (m_expr_pos_info.find(e) == m_expr_pos_info.end()) {
+                    save(e, p);
+                    return true;
+                } else {
+                    return false; // do not search children...
+                }
+            });
+    }
+
     bool is_curr_begin_expr() const {
         switch (curr()) {
         case scanner::token::RightParen:
@@ -955,7 +966,8 @@ class parser::imp {
                     if (is_expr(L, -1)) {
                         expr r = to_expr(L, -1);
                         lua_pop(L, 1);
-                        return save(r, p);
+                        propagage_position(r, p);
+                        return r;
                     } else {
                         lua_pop(L, 1);
                         throw parser_error("failed to execute macro", p);
@@ -971,7 +983,7 @@ class parser::imp {
         luaref proc                    = m.second;
         macro_arg_stack args;
         return parse_macro(arg_kinds, proc, args, p);
-            }
+    }
 
     /**
         \brief Parse an identifier that has a "null denotation" (See