From 9b5568759775c4bcb5bbeb83efe2bf12a5ee7813 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 18 Oct 2019 13:10:13 +0200 Subject: [PATCH] fix: show #eval errors --- src/frontends/lean/builtin_cmds.cpp | 12 +++++++++--- tests/playground/cmdparsertest1.lean | 2 +- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 8c88b38206..ecb656c505 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -357,17 +357,23 @@ static environment eval_cmd(parser & p) { // run `IO Unit` object * args[] = { io_mk_world() }; + object_ref r; if (p.profiling()) { timeit timer(out.get_text_stream().get_stream(), "eval time"); - // NOTE: no need to free `()` - ir::run_boxed(new_env, fn_name, &args[0]); + r = object_ref(ir::run_boxed(new_env, fn_name, &args[0])); } else { - ir::run_boxed(new_env, fn_name, &args[0]); + r = object_ref(ir::run_boxed(new_env, fn_name, &args[0])); } std::cout.rdbuf(saved_cout); out.report(); + if (io_result_is_error(r.raw())) { + message_builder msg = p.mk_message(p.cmd_pos(), p.pos(), ERROR); + msg << string_to_std(io_result_get_error(r.raw())); + msg.report(); + } + return p.env(); } diff --git a/tests/playground/cmdparsertest1.lean b/tests/playground/cmdparsertest1.lean index b99f2b0f74..31e661630c 100644 --- a/tests/playground/cmdparsertest1.lean +++ b/tests/playground/cmdparsertest1.lean @@ -1,4 +1,4 @@ -import init.lean.parser.command +import Init.Lean.Parser.Command open Lean open Lean.Parser