From a30603405cd4d1b320f2b045ff7dcec9af36c299 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 15 Jul 2016 15:10:04 -0400
Subject: [PATCH] feat(library/vm/vm): add scope_vm_state

---
 src/library/vm/vm.cpp | 9 +++++++++
 src/library/vm/vm.h   | 8 ++++++++
 2 files changed, 17 insertions(+)

diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index 8c492974a3..b5b561a09a 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -1004,6 +1004,15 @@ void vm_state::invoke_builtin(vm_decl const & d) {
 
 LEAN_THREAD_VALUE(vm_state *, g_vm_state, nullptr);
 
+scope_vm_state::scope_vm_state(vm_state & s):
+    m_prev(g_vm_state) {
+    g_vm_state = &s;
+}
+
+scope_vm_state::~scope_vm_state() {
+    g_vm_state = m_prev;
+}
+
 void vm_state::invoke_cfun(vm_decl const & d) {
     flet<vm_state *> Set(g_vm_state, this);
     auto & S       = m_stack;
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index 9ade0e3d30..e8368a48a7 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -583,6 +583,14 @@ public:
     }
 };
 
+/** \brief Helper class for setting thread local vm_state object */
+class scope_vm_state {
+    vm_state * m_prev;
+public:
+    scope_vm_state(vm_state & s);
+    ~scope_vm_state();
+};
+
 /** \brief Return reference to thread local VM state object. */
 vm_state const & get_vm_state();