michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(frontends/lean/parser): use std::function

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-02 06:53:34 -08:00
parent 5540fc861a
commit d7493ea86c
2 changed files with 11 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/frontends/lean/parser_imp.cpp
View file

@ -31,6 +31,16 @@ bool get_parser_verbose(options const & opts) { return opts.get_bool(g_
bool get_parser_show_errors(options const & opts) { return opts.get_bool(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); }
// ==========================================
void parser_imp::code_with_callbacks(std::function<void()> && f) {
m_script_state->apply([&](lua_State * L) {
set_io_state set1(L, m_io_state);
set_environment set2(L, m_env);
m_script_state->exec_unprotected([&]() {
f();
});
});
}
parser_imp::mk_scope::mk_scope(parser_imp & fn):
m_fn(fn),
m_scope(fn.m_local_decls),

11
src/frontends/lean/parser_imp.h
View file

@ -93,16 +93,7 @@ class parser_imp {
});
}
template<typename F>
void code_with_callbacks(F && f) {
m_script_state->apply([&](lua_State * L) {
set_io_state set1(L, m_io_state);
set_environment set2(L, m_env);
m_script_state->exec_unprotected([&]() {
f();
});
});
}
void code_with_callbacks(std::function<void()> && f);
/**
\brief Auxiliar struct for creating/destroying a new scope for