From 008b43d92affa7647990491fb4f808f3b7cbdf7a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Aug 2014 18:09:31 -0700 Subject: [PATCH] refactor(frontends/lean/info_manager): add method info_data::compare Signed-off-by: Leonardo de Moura --- src/frontends/lean/info_manager.cpp | 15 +++++++++++---- src/frontends/lean/info_manager.h | 1 + 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 24f3ef6207..88a45d1225 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -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 { diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index dcec244c17..e2da02c41d 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -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 &) {} };