diff --git a/stage0/src/Init/Lean/Message.lean b/stage0/src/Init/Lean/Message.lean index f300e5b1a4..264440e025 100644 --- a/stage0/src/Init/Lean/Message.lean +++ b/stage0/src/Init/Lean/Message.lean @@ -131,7 +131,6 @@ mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column | MessageSeverity.error => "error: ") ++ (if msg.caption == "" then "" else msg.caption ++ ":\n") ++ toString (fmt msg.data)) - instance : Inhabited Message := ⟨{ fileName := "", pos := ⟨0, 1⟩, data := arbitrary _}⟩ diff --git a/stage0/src/library/messages.cpp b/stage0/src/library/messages.cpp index d2b9184f1c..fd72baee9d 100644 --- a/stage0/src/library/messages.cpp +++ b/stage0/src/library/messages.cpp @@ -12,6 +12,7 @@ namespace lean { extern "C" object * lean_mk_message(object * filename, object * pos, object * end_pos, uint8 severity, object * caption, object * text); extern "C" uint8 lean_message_severity(object * msg); +extern "C" object * lean_message_string(object * msg); message::message(std::string const & filename, pos_info const & pos, optional const & end_pos, message_severity severity, std::string const & caption, std::string const & text) : @@ -28,6 +29,10 @@ message_severity message::get_severity() const { return static_cast(lean_message_severity(to_obj_arg())); } +std::string message::get_text() const { + return string_ref(lean_message_string(to_obj_arg())).to_std_string(); +} + std::ostream & operator<<(std::ostream & out, message const & msg) { if (msg.get_severity() != INFORMATION) { out << msg.get_filename() << ":" << msg.get_pos().first << ":" << msg.get_pos().second << ": "; diff --git a/stage0/src/library/messages.h b/stage0/src/library/messages.h index c3717bf9ef..856bf39ad1 100644 --- a/stage0/src/library/messages.h +++ b/stage0/src/library/messages.h @@ -63,7 +63,7 @@ public: } message_severity get_severity() const; std::string get_caption() const { return static_cast(cnstr_get_ref(*this, 3)).to_std_string(); } - std::string get_text() const { return static_cast(cnstr_get_ref(*this, 4)).to_std_string(); } + std::string get_text() const; bool is_error() const { return get_severity() >= ERROR; } };