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

chore(library/io_state): avoid thread local storage

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-16 12:08:11 -08:00
parent a076f0003d
commit c35f2a2098
2 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/library/io_state.cpp
View file

@ -81,15 +81,14 @@ scope_global_ios::~scope_global_ios() {
g_ios = m_old_ios;
}
MK_THREAD_LOCAL_GET_DEF(std::string, get_what_str);
char const * formatted_exception::what() const noexcept {
options const & opts = get_global_ios().get_options();
std::ostringstream out;
out << mk_pair(m_fmt, opts);
std::string & r = get_what_str();
r = out.str();
return r.c_str();
if (!m_what_buffer) {
options const & opts = get_global_ios().get_options();
std::ostringstream out;
out << mk_pair(m_fmt, opts);
const_cast<formatted_exception*>(this)->m_what_buffer = out.str();
}
return m_what_buffer->c_str();
}
options const & get_options_from_ios(io_state const & ios) {

7
src/library/io_state.h
View file

@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include "util/output_channel.h"
#include "util/sexpr/options.h"
#include "util/exception_with_pos.h"
@ -61,8 +61,9 @@ io_state const & get_global_ios();
This is slightly different from ext_exception where the format object is built on demand. */
class formatted_exception : public exception_with_pos {
protected:
optional<pos_info> m_pos;
format m_fmt;
optional<pos_info> m_pos;
format m_fmt;
optional<std::string> m_what_buffer;
public:
explicit formatted_exception(format const & fmt):m_fmt(fmt) {}
formatted_exception(optional<pos_info> const & p, format const & fmt):m_pos(p), m_fmt(fmt) {}