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

refactor(frontends/lean/info_manager): add method info_data::compare

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-15 18:09:31 -07:00
parent 14d6b6d043
commit 008b43d92a
2 changed files with 12 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/frontends/lean/info_manager.cpp
View file

@ -15,11 +15,18 @@ struct tmp_info_data : public info_data {
virtual void display(io_state_stream const &) const { lean_unreachable(); } // LCOV_EXCL_LINE
};
int info_data::compare(info_data const & d) const {
if (m_line != d.m_line)
return m_line < d.m_line ? -1 : 1;
if (m_column != d.m_column)
return m_column < d.m_column ? -1 : 1;
if (typeid(*this) != typeid(d))
return typeid(*this).before(typeid(d)) ? -1 : 1;
return 0;
}
bool operator<(info_data const & i1, info_data const & i2) {
if (i1.get_line() != i2.get_line())
return i1.get_line() < i2.get_line();
else
return i1.get_column() < i2.get_column();
return i1.compare(i2) < 0;
}
void type_info_data::display(io_state_stream const & ios) const {

1
src/frontends/lean/info_manager.h
View file

@ -23,6 +23,7 @@ public:
unsigned get_line() const { return m_line; }
unsigned get_column() const { return m_column; }
bool eq_pos(unsigned line, unsigned col) const { return m_line == line && m_column == col; }
virtual int compare(info_data const & d) const;
virtual void display(io_state_stream const & ios) const = 0;
virtual void instantiate(substitution &) {}
};