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

refactor(library/io_state_stream): avoid references in io_state_stream object

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-25 20:16:58 -07:00
parent 4f3ce09b57
commit 7e759e6773
2 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/io_state.h
View file

@ -32,6 +32,8 @@ public:
options get_options() const { return m_options; }
formatter_factory const & get_formatter_factory() const { return m_formatter_factory; }
std::shared_ptr<output_channel> const & get_regular_channel_ptr() const { return m_regular_channel; }
std::shared_ptr<output_channel> const & get_diagnostic_channel_ptr() const { return m_diagnostic_channel; }
output_channel & get_regular_channel() const { return *m_regular_channel; }
output_channel & get_diagnostic_channel() const { return *m_diagnostic_channel; }
std::ostream & get_regular_stream() const { return m_regular_channel->get_stream(); }

14
src/library/io_state_stream.h
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include "kernel/environment.h"
#include "kernel/ext_exception.h"
#include "kernel/abstract_type_context.h"
#include "library/generic_exception.h"
@ -16,15 +17,16 @@ namespace lean {
/** \brief Base class for \c regular and \c diagnostic wrapper classes. */
class io_state_stream {
protected:
environment const & m_env;
formatter m_formatter;
output_channel & m_stream;
io_state_stream(environment const & env, formatter const & fmt, output_channel & s):m_env(env), m_formatter(fmt), m_stream(s) {}
environment m_env;
formatter m_formatter;
std::shared_ptr<output_channel> m_stream;
io_state_stream(environment const & env, formatter const & fmt, std::shared_ptr<output_channel> const & s):
m_env(env), m_formatter(fmt), m_stream(s) {}
public:
io_state_stream(environment const & env, io_state const & ios, abstract_type_context & ctx, bool regular = true):
m_env(env), m_formatter(ios.get_formatter_factory()(env, ios.get_options(), ctx)),
m_stream(regular ? ios.get_regular_channel() : ios.get_diagnostic_channel()) {}
std::ostream & get_stream() const { return m_stream.get_stream(); }
m_stream(regular ? ios.get_regular_channel_ptr() : ios.get_diagnostic_channel_ptr()) {}
std::ostream & get_stream() const { return m_stream->get_stream(); }
void flush() { get_stream().flush(); }
formatter const & get_formatter() const { return m_formatter; }
options get_options() const { return m_formatter.get_options(); }