diff --git a/src/frontends/lean/elaborator_context.cpp b/src/frontends/lean/elaborator_context.cpp
index 31e8a1e6dd..d3975609aa 100644
--- a/src/frontends/lean/elaborator_context.cpp
+++ b/src/frontends/lean/elaborator_context.cpp
@@ -44,14 +44,14 @@ bool get_elaborator_coercions(options const & opts) {
 // ==========================================
 
 elaborator_context::elaborator_context(environment const & env, options const & opts, local_level_decls const & lls,
-                                       pos_info_provider const * pp, info_manager * info, bool check_unassigned):
-    m_env(env), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) {
+                                       info_manager * info, bool check_unassigned):
+    m_env(env), m_lls(lls), m_info_manager(info), m_check_unassigned(check_unassigned) {
     set_options(opts);
 }
 
 elaborator_context::elaborator_context(elaborator_context const & ctx, options const & o):
-    m_env(ctx.m_env), m_lls(ctx.m_lls), m_pos_provider(ctx.m_pos_provider),
-    m_info_manager(ctx.m_info_manager), m_check_unassigned(ctx.m_check_unassigned) {
+    m_env(ctx.m_env), m_lls(ctx.m_lls), m_info_manager(ctx.m_info_manager),
+    m_check_unassigned(ctx.m_check_unassigned) {
     set_options(o);
 }
 
diff --git a/src/frontends/lean/elaborator_context.h b/src/frontends/lean/elaborator_context.h
index c5159084f1..c0800c4382 100644
--- a/src/frontends/lean/elaborator_context.h
+++ b/src/frontends/lean/elaborator_context.h
@@ -21,7 +21,6 @@ class elaborator_context {
 
     environment               m_env;
     local_level_decls         m_lls; // local universe levels
-    pos_info_provider const * m_pos_provider;
     info_manager *            m_info_manager;
     // configuration
     options                   m_options;
@@ -47,7 +46,7 @@ class elaborator_context {
     bool has_show_hole_at(unsigned & line, unsigned & col) const;
 public:
     elaborator_context(environment const & env, options const & opts, local_level_decls const & lls,
-                       pos_info_provider const * pp = nullptr, info_manager * info = nullptr,
+                       info_manager * info = nullptr,
                        bool check_unassigned = true);
     elaborator_context(elaborator_context const & ctx, options const & o);
 };
diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp
index 0dcca0ae0c..cafa35e874 100644
--- a/src/frontends/lean/old_elaborator.cpp
+++ b/src/frontends/lean/old_elaborator.cpp
@@ -211,6 +211,10 @@ optional<expr> old_elaborator::mvar_to_meta(expr const & mvar) {
         return none_expr();
 }
 
+static parser_pos_provider * pip() {
+    return get_parser_pos_provider();
+}
+
 /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */
 void old_elaborator::save_type_data(expr const & e, expr const & r) {
     if (!m_no_info && infom() && pip() &&
@@ -342,7 +346,7 @@ expr old_elaborator::mk_placeholder_meta(optional<name> const & suffix, optional
     if (is_inst_implicit) {
         auto ec = mk_class_instance_elaborator(
             env(), get_global_ios(), m_context, suffix,
-            true, is_strict, type, g, m_ctx.m_pos_provider);
+            true, is_strict, type, g, nullptr);
         register_meta(ec.first);
         cs += ec.second;
         return ec.first;
diff --git a/src/frontends/lean/old_elaborator.h b/src/frontends/lean/old_elaborator.h
index e6416bdd25..e08eed7fc4 100644
--- a/src/frontends/lean/old_elaborator.h
+++ b/src/frontends/lean/old_elaborator.h
@@ -73,7 +73,6 @@ class old_elaborator : public coercion_info_manager {
     environment const & env() const { return m_ctx.m_env; }
     local_level_decls const & lls() const { return m_ctx.m_lls; }
     info_manager * infom() const { return m_ctx.m_info_manager; }
-    pos_info_provider const * pip() const { return m_ctx.m_pos_provider; }
     bool check_unassigned() const { return m_ctx.m_check_unassigned; }
 
     expr mk_local(name const & n, expr const & t, binder_info const & bi);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 5f803c7e16..23ad9fd6cb 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -47,6 +47,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/util.h"
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/info_annotation.h"
+#include "frontends/lean/parser_pos_provider.h"
 // #include "frontends/lean/parse_rewrite_tactic.h"
 // #include "frontends/lean/parse_tactic_location.h"
 #include "frontends/lean/update_environment_exception.h"
@@ -897,24 +898,21 @@ level parser::parse_level(unsigned rbp) {
     return left;
 }
 
-elaborator_context parser::mk_elaborator_context(pos_info_provider const &  pp, bool check_unassigned) {
-    return elaborator_context(m_env, get_options(), m_local_level_decls, &pp, m_info_manager, check_unassigned);
+elaborator_context parser::mk_elaborator_context(bool check_unassigned) {
+    return elaborator_context(m_env, get_options(), m_local_level_decls, m_info_manager, check_unassigned);
 }
 
-elaborator_context parser::mk_elaborator_context(environment const & env, pos_info_provider const & pp) {
-    return elaborator_context(env, get_options(), m_local_level_decls, &pp, m_info_manager, true);
+elaborator_context parser::mk_elaborator_context(environment const & env) {
+    return elaborator_context(env, get_options(), m_local_level_decls, m_info_manager, true);
 }
 
-elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls,
-                                                 pos_info_provider const & pp) {
-    return elaborator_context(env, get_options(), lls, &pp, m_info_manager, true);
+elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls) {
+    return elaborator_context(env, get_options(), lls, m_info_manager, true);
 }
 
 std::tuple<expr, level_param_names> parser::elaborate(expr const & e) {
-    parser_pos_provider pip = get_pos_provider();
     bool check_unassigned   = true;
-    parser_pos_provider pp  = get_pos_provider();
-    elaborator_context ectx = mk_elaborator_context(pp, check_unassigned);
+    elaborator_context ectx = mk_elaborator_context(check_unassigned);
     return ::lean::elaborate(ectx, m_local_context, e);
 }
 
@@ -922,8 +920,7 @@ std::tuple<expr, level_param_names> parser::old_elaborate_relaxed(expr const & e
     bool check_unassigned = false;
     bool ensure_type      = false;
     bool nice_mvar_names  = true;
-    parser_pos_provider pp = get_pos_provider();
-    elaborator_context env = mk_elaborator_context(pp, check_unassigned);
+    elaborator_context env = mk_elaborator_context(check_unassigned);
     auto r = ::lean::elaborate(env, ctx, e, ensure_type, nice_mvar_names);
     m_pre_info_manager.clear();
     return r;
@@ -932,8 +929,7 @@ std::tuple<expr, level_param_names> parser::old_elaborate_relaxed(expr const & e
 std::tuple<expr, level_param_names> parser::old_elaborate(expr const & e, list<expr> const & ctx) {
     bool check_unassigned = true;
     bool ensure_type      = false;
-    parser_pos_provider pp = get_pos_provider();
-    elaborator_context env = mk_elaborator_context(pp, check_unassigned);
+    elaborator_context env = mk_elaborator_context(check_unassigned);
     auto r = ::lean::elaborate(env, ctx, e, ensure_type);
     m_pre_info_manager.clear();
     return r;
@@ -942,8 +938,7 @@ std::tuple<expr, level_param_names> parser::old_elaborate(expr const & e, list<e
 std::tuple<expr, level_param_names> parser::old_elaborate_type(expr const & e, list<expr> const & ctx, bool clear_pre_info) {
     bool check_unassigned = true;
     bool ensure_type      = true;
-    parser_pos_provider pp = get_pos_provider();
-    elaborator_context env = mk_elaborator_context(pp, check_unassigned);
+    elaborator_context env = mk_elaborator_context(check_unassigned);
     auto r = ::lean::elaborate(env, ctx, e, ensure_type);
     if (clear_pre_info)
         m_pre_info_manager.clear();
@@ -951,8 +946,7 @@ std::tuple<expr, level_param_names> parser::old_elaborate_type(expr const & e, l
 }
 
 std::tuple<expr, level_param_names> parser::old_elaborate_at(environment const & env, expr const & e) {
-    parser_pos_provider pp = get_pos_provider();
-    elaborator_context eenv = mk_elaborator_context(env, pp);
+    elaborator_context eenv = mk_elaborator_context(env);
     auto r = ::lean::elaborate(eenv, list<expr>(), e);
     m_pre_info_manager.clear();
     return r;
@@ -960,8 +954,7 @@ std::tuple<expr, level_param_names> parser::old_elaborate_at(environment const &
 
 auto parser::old_elaborate_definition(name const & n, expr const & t, expr const & v)
     -> std::tuple<expr, expr, level_param_names> {
-    parser_pos_provider pp = get_pos_provider();
-    elaborator_context eenv = mk_elaborator_context(pp);
+    elaborator_context eenv = mk_elaborator_context();
     auto r = ::lean::elaborate(eenv, n, t, v);
     m_pre_info_manager.clear();
     return r;
@@ -970,8 +963,7 @@ auto parser::old_elaborate_definition(name const & n, expr const & t, expr const
 auto parser::old_elaborate_definition_at(environment const & env, local_level_decls const & lls,
                                      name const & n, expr const & t, expr const & v)
 -> std::tuple<expr, expr, level_param_names> {
-    parser_pos_provider pp = get_pos_provider();
-    elaborator_context eenv = mk_elaborator_context(env, lls, pp);
+    elaborator_context eenv = mk_elaborator_context(env, lls);
     auto r = ::lean::elaborate(eenv, n, t, v);
     m_pre_info_manager.clear();
     return r;
@@ -1812,6 +1804,8 @@ void parser::parse_command() {
     m_last_cmd_pos = pos();
     name const & cmd_name = get_token_info().value();
     m_cmd_token = get_token_info().token();
+    parser_pos_provider ppp(parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos));
+    scope_parser_pos_provider scope(ppp);
     if (auto it = cmds().find(cmd_name)) {
         lazy_type_context tc(m_env, get_options());
         scope_global_ios scope1(m_ios);
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 53e1970092..4926c55a16 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "kernel/environment.h"
 #include "kernel/expr_maps.h"
+#include "kernel/pos_info_provider.h"
 #include "library/io_state.h"
 #include "library/io_state_stream.h"
 #include "library/local_context.h"
@@ -23,7 +24,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/local_decls.h"
 #include "frontends/lean/local_level_decls.h"
 #include "frontends/lean/parser_config.h"
-#include "frontends/lean/parser_pos_provider.h"
 #include "frontends/lean/theorem_queue.h"
 #include "frontends/lean/info_manager.h"
 
@@ -228,10 +228,9 @@ class parser {
     void commit_info(unsigned line, unsigned col);
     void commit_info() { commit_info(m_scanner.get_line(), m_scanner.get_pos()); }
 
-    elaborator_context mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned = true);
-    elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp);
-    elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls,
-                                             pos_info_provider const & pp);
+    elaborator_context mk_elaborator_context(bool check_unassigned = true);
+    elaborator_context mk_elaborator_context(environment const & env);
+    elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls);
 
     void init_stop_at(options const & opts);
 
@@ -512,9 +511,6 @@ public:
     bool used_sorry() const { return m_used_sorry; }
     void declare_sorry();
 
-    parser_pos_provider get_pos_provider() const {
-        return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos);
-    }
     void display_information_pos(pos_info p);
     void display_warning_pos(pos_info p);
 
diff --git a/src/frontends/lean/parser_pos_provider.cpp b/src/frontends/lean/parser_pos_provider.cpp
index 828eb20e59..d9e69b7eb5 100644
--- a/src/frontends/lean/parser_pos_provider.cpp
+++ b/src/frontends/lean/parser_pos_provider.cpp
@@ -32,4 +32,13 @@ pos_info parser_pos_provider::get_some_pos() const {
 char const * parser_pos_provider::get_file_name() const {
     return m_strm_name.c_str();
 }
+
+LEAN_THREAD_PTR(parser_pos_provider, g_ppp);
+
+scope_parser_pos_provider::scope_parser_pos_provider(parser_pos_provider & ppp):m_old_ppp(g_ppp) { g_ppp = &ppp; }
+scope_parser_pos_provider::~scope_parser_pos_provider() { g_ppp = m_old_ppp; }
+
+parser_pos_provider * get_parser_pos_provider() {
+    return g_ppp;
+}
 }
diff --git a/src/frontends/lean/parser_pos_provider.h b/src/frontends/lean/parser_pos_provider.h
index 3d6a561a7f..5c3c4eed11 100644
--- a/src/frontends/lean/parser_pos_provider.h
+++ b/src/frontends/lean/parser_pos_provider.h
@@ -25,4 +25,13 @@ public:
     virtual pos_info get_some_pos() const;
     virtual char const * get_file_name() const;
 };
+
+class scope_parser_pos_provider {
+    parser_pos_provider * m_old_ppp;
+public:
+    scope_parser_pos_provider(parser_pos_provider & ppp);
+    ~scope_parser_pos_provider();
+};
+
+parser_pos_provider * get_parser_pos_provider();
 }