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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-25 14:22:57 -08:00
parent cfd7fc8a87
commit c10764b13e
3 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
stage0/src/Init/Lean/Message.lean
View file

@ -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 _}⟩

5
stage0/src/library/messages.cpp
View file

@ -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<pos_info> 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<message_severity>(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 << ": ";

2
stage0/src/library/messages.h
View file

@ -63,7 +63,7 @@ public:
}
message_severity get_severity() const;
std::string get_caption() const { return static_cast<string_ref const &>(cnstr_get_ref(*this, 3)).to_std_string(); }
std::string get_text() const { return static_cast<string_ref const &>(cnstr_get_ref(*this, 4)).to_std_string(); }
std::string get_text() const;
bool is_error() const { return get_severity() >= ERROR; }
};