michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/io_state): add constructor for copying io_state, but replacing channels

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-24 13:18:28 -07:00
parent 49b2bb209d
commit 5df2331159
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/io_state.cpp
View file

@ -20,6 +20,12 @@ io_state::io_state(options const & opts, formatter const & fmt):
m_regular_channel(std::make_shared<stdout_channel>()),
m_diagnostic_channel(std::make_shared<stderr_channel>()) {
}
io_state::io_state(io_state const & ios, std::shared_ptr<output_channel> const & r, std::shared_ptr<output_channel> const d):
m_options(ios.m_options),
m_formatter(ios.m_formatter),
m_regular_channel(r),
m_diagnostic_channel(d) {
}
io_state::~io_state() {}

1
src/library/io_state.h
View file

@ -25,6 +25,7 @@ class io_state {
public:
io_state(formatter const & fmt);
io_state(options const & opts, formatter const & fmt);
io_state(io_state const & ios, std::shared_ptr<output_channel> const & r, std::shared_ptr<output_channel> const d);
~io_state();
options get_options() const { return m_options; }