From 340d643d896240f5f88a985cb548e32bc41e2cc5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Dec 2013 16:53:51 -0800
Subject: [PATCH] fix(library/kernel_bindings): make sure that when a formatter
 is invoked and it has a reference to an environment object, we get a
 read-only lock to the environment object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/pp.cpp       |  2 ++
 src/kernel/formatter.h          | 10 ++++++++--
 src/library/kernel_bindings.cpp | 13 ++++++++++++-
 3 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 0a68961ae..343565477 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1378,6 +1378,8 @@ public:
                       });
         return r;
     }
+
+    virtual optional<environment> get_environment() const { return optional<environment>(env()); }
 };
 
 formatter mk_pp_formatter(environment const & env) {
diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h
index 7afce2293..79c548bad 100644
--- a/src/kernel/formatter.h
+++ b/src/kernel/formatter.h
@@ -8,10 +8,9 @@ Author: Leonardo de Moura
 #include <memory>
 #include "util/sexpr/options.h"
 #include "kernel/context.h"
+#include "kernel/environment.h"
 
 namespace lean {
-class environment;
-class object;
 /**
    \brief API for formatting expressions, contexts and environments.
 */
@@ -34,6 +33,12 @@ public:
     virtual format operator()(object const & obj, options const & opts) = 0;
     /** \brief Format the given environment */
     virtual format operator()(environment const & env, options const & opts) = 0;
+
+    /**
+        \brief Return environment object associated with this formatter.
+        Not every formatter has an associated environment object.
+    */
+    virtual optional<environment> get_environment() { return optional<environment>(); }
 };
 /**
    \brief Smart-pointer for the actual formatter object (aka \c formatter_cell).
@@ -47,6 +52,7 @@ public:
     format operator()(context const & c, expr const & e, bool format_ctx = false, options const & opts = options()) const { return (*m_cell)(c, e, format_ctx, opts); }
     format operator()(object const & obj, options const & opts = options()) const { return (*m_cell)(obj, opts); }
     format operator()(environment const & env, options const & opts = options()) const { return (*m_cell)(env, opts); }
+    optional<environment> get_environment() { return m_cell->get_environment(); }
 
     template<typename FCell>
     friend formatter mk_formatter(FCell && fcell) {
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index f5245e7d8..41956abf9 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -815,7 +815,7 @@ DECL_UDATA(formatter)
     throw exception("invalid formatter invocation, the acceptable arguments are: (expr, options?), (context, options?), (context, expr, bool? options?), (kernel object, options?), (environment, options?)");
 }
 
-static int formatter_call(lua_State * L) {
+static int formatter_call_core(lua_State * L) {
     int nargs = lua_gettop(L);
     formatter & fmt = to_formatter(L, 1);
     options opts = get_global_options(L);
@@ -849,6 +849,17 @@ static int formatter_call(lua_State * L) {
     }
 }
 
+static int formatter_call(lua_State * L) {
+    formatter & fmt = to_formatter(L, 1);
+    optional<environment> env = fmt.get_environment();
+    if (env) {
+        read_only_environment ro_env(*env);
+        return formatter_call_core(L);
+    } else {
+        return formatter_call_core(L);
+    }
+}
+
 static const struct luaL_Reg formatter_m[] = {
     {"__gc",            formatter_gc}, // never throws
     {"__call",          safe_function<formatter_call>},