diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index c2b85a511e..fbffcb803e 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -94,10 +94,10 @@ def getPrintMessageEndPos (opts : Options) : Bool := opts.getBool `printMessageEndPos false @[export lean_run_frontend] -def runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) : IO (Environment × Bool) := do +def runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) (trustLevel : UInt32 := 0) : IO (Environment × Bool) := do let inputCtx := Parser.mkInputContext input fileName let (header, parserState, messages) ← Parser.parseHeader inputCtx - let (env, messages) ← processHeader header opts messages inputCtx + let (env, messages) ← processHeader header opts messages inputCtx trustLevel let env := env.setMainModule mainModuleName let s ← IO.processCommands inputCtx parserState (Command.mkState env messages opts) for msg in s.commandState.messages.toList do diff --git a/src/util/shell.cpp b/src/util/shell.cpp index 5c1a537e7e..921f9cffce 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -336,10 +336,10 @@ void load_library(std::string path) { } namespace lean { -extern "C" object * lean_run_frontend(object * input, object * opts, object * filename, object * main_module_name, object * w); -pair_ref run_new_frontend(std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name) { +extern "C" object * lean_run_frontend(object * input, object * opts, object * filename, object * main_module_name, uint32_t trust_level, object * w); +pair_ref run_new_frontend(std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name, uint32_t trust_level) { return get_io_result>( - lean_run_frontend(mk_string(input), opts.to_obj_arg(), mk_string(file_name), main_module_name.to_obj_arg(), io_mk_world())); + lean_run_frontend(mk_string(input), opts.to_obj_arg(), mk_string(file_name), main_module_name.to_obj_arg(), trust_level, io_mk_world())); } /* def workerMain : Options → IO UInt32 */ @@ -647,7 +647,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { if (!main_module_name) main_module_name = name("_stdin"); - pair_ref r = run_new_frontend(contents, opts, mod_fn, *main_module_name); + pair_ref r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl); env = r.fst(); bool ok = unbox(r.snd().raw());