max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/vm/vm_io): capture put_str/put_nat output in server mode

Browse source
This commit is contained in:
Sebastian Ullrich 2016-10-19 12:06:35 -04:00 • committed by Leonardo de Moura
parent 133b70c0e3
commit 044b989679
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/vm/vm_io.cpp
View file

@ -6,20 +6,22 @@ Author: Leonardo de Moura
*/
#include <string>
#include <iostream>
#include "library/io_state.h"
#include "library/tactic/tactic_state.h"
#include "library/vm/vm.h"
#include "library/vm/vm_string.h"
namespace lean {
vm_obj put_str(vm_obj const & str, vm_obj const &) {
std::cout << to_string(str);
get_global_ios().get_regular_stream() << to_string(str);
return mk_vm_unit();
}
vm_obj put_nat(vm_obj const & n, vm_obj const &) {
if (is_simple(n))
std::cout << cidx(n);
get_global_ios().get_regular_stream() << cidx(n);
else
std::cout << to_mpz(n);
get_global_ios().get_regular_stream() << to_mpz(n);
return mk_vm_unit();
}