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

feat(frontends/lean): allow the user to set the trust_imported flag when creating environments using Lua

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-12 16:46:53 -08:00
parent 4d9eb4ac6c
commit 582569b793
3 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/register_module.cpp
View file

@ -125,8 +125,19 @@ static int parse_lean_cmds(lua_State * L) {
}
}
static bool g_default_trust_imported = false;
void set_default_trust_imported_for_lua(bool f) {
g_default_trust_imported = f;
}
static int mk_environment(lua_State * L) {
int nargs = lua_gettop(L);
environment env;
if (nargs == 0)
env->set_trusted_imported(g_default_trust_imported);
else
env->set_trusted_imported(lua_toboolean(L, 1));
io_state ios = init_frontend(env);
return push_environment(L, env);
}

1
src/frontends/lean/register_module.h
View file

@ -9,4 +9,5 @@ Author: Leonardo de Moura
namespace lean {
void open_frontend_lean(lua_State * L);
void register_frontend_lean_module();
void set_default_trust_imported_for_lua(bool f);
}

2
src/shell/lean.cpp
View file

@ -26,6 +26,7 @@ Author: Leonardo de Moura
#include "frontends/lean/parser.h"
#include "frontends/lean/shell.h"
#include "frontends/lean/frontend.h"
#include "frontends/lean/register_module.h"
#include "frontends/lua/register_modules.h"
#include "version.h"
#include "githash.h" // NOLINT
@ -157,6 +158,7 @@ int main(int argc, char ** argv) {
break;
case 't':
trust_imported = true;
lean::set_default_trust_imported_for_lua(true);
break;
case 'q':
quiet = true;