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

feat(library/io_state): add default constructor to io_state

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-11 13:18:22 -07:00
parent 80fd14b39e
commit c7c35becb2
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/io_state.cpp
View file

@ -14,6 +14,8 @@ io_state const & get_dummy_ios() {
return g_dummy_ios;
}
io_state::io_state():io_state(mk_print_formatter_factory()) {}
io_state::io_state(formatter_factory const & fmtf):
m_formatter_factory(fmtf),
m_regular_channel(std::make_shared<stdout_channel>()),

1
src/library/io_state.h
View file

@ -23,6 +23,7 @@ class io_state {
std::shared_ptr<output_channel> m_regular_channel;
std::shared_ptr<output_channel> m_diagnostic_channel;
public:
io_state();
io_state(formatter_factory const & fmtf);
io_state(options const & opts, formatter_factory const & fmtf);
io_state(io_state const & ios, std::shared_ptr<output_channel> const & r, std::shared_ptr<output_channel> const d);