From 044b989679de9b9ddd10934c702dfd352416a940 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Oct 2016 12:06:35 -0400
Subject: [PATCH] fix(library/vm/vm_io): capture put_str/put_nat output in
 server mode

---
 src/library/vm/vm_io.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp
index 3095a0f91c..3c7b315f06 100644
--- a/src/library/vm/vm_io.cpp
+++ b/src/library/vm/vm_io.cpp
@@ -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();
 }