diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 0495719931..636011617c 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -336,10 +336,20 @@ struct stream_buffer_delete { } }; -flet lean_redirect_stdout(object * new_stdout); +obj_res lean_redirect_stdout(obj_arg new_stdout); lean_object * lean_io_wrap_handle(FILE *hfile); lean_object *& get_handle_current_stdout(); +struct redirect_helper { + object_ref m_old_fp; + redirect_helper(object_ref const & new_fp): + m_old_fp(lean_redirect_stdout(new_fp.to_obj_arg())) { + } + ~redirect_helper() { + lean_dec(lean_redirect_stdout(m_old_fp.to_obj_arg())); + } +}; + static environment eval_cmd(parser & p) { transient_cmd_scope cmd_scope(p); auto pos = p.pos(); @@ -399,8 +409,8 @@ static environment eval_cmd(parser & p) { object_ref r; try { - object_ref newFP(lean_io_wrap_handle(fp)); - flet oldFP(lean_redirect_stdout(newFP.raw())); + object_ref new_fp(lean_io_wrap_handle(fp)); + redirect_helper helper(new_fp); if (p.profiling()) { timeit timer(out.get_text_stream().get_stream(), "eval time"); r = object_ref(ir::run_boxed(new_env, fn_name, args.size(), &args[0])); diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 3e41f16c0a..0fb292ec47 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -22,7 +22,6 @@ Author: Leonardo de Moura #include #include #include "util/io.h" -#include "runtime/flet.h" #include "runtime/utf8.h" #include "runtime/object.h" #include "runtime/thread.h" @@ -145,8 +144,10 @@ MK_THREAD_LOCAL_GET(object *, get_handle_current_stdout, g_handle_stdout); MK_THREAD_LOCAL_GET(object *, get_handle_current_stderr, g_handle_stderr); MK_THREAD_LOCAL_GET(object *, get_handle_current_stdin, g_handle_stdin); -flet lean_redirect_stdout(object * new_stdout) { - return flet(get_handle_current_stdout(), new_stdout); +obj_res lean_redirect_stdout(obj_arg new_stdout) { + obj_res r = get_handle_current_stdout(); + get_handle_current_stdout() = new_stdout; + return r; } /* getStdout : IO FS.Handle */