From e0eeb7c8d5efc241c523070c91b4dcd47a8e8466 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Dec 2013 12:52:31 -0800
Subject: [PATCH] feat(frontends/lean/operator_info): add << for diagnostic and
 regular streams

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/operator_info.cpp | 10 ++++++++++
 src/frontends/lean/operator_info.h   |  4 ++++
 2 files changed, 14 insertions(+)

diff --git a/src/frontends/lean/operator_info.cpp b/src/frontends/lean/operator_info.cpp
index 39dcd8d20..b96c788ae 100644
--- a/src/frontends/lean/operator_info.cpp
+++ b/src/frontends/lean/operator_info.cpp
@@ -183,4 +183,14 @@ std::ostream & operator<<(std::ostream & out, operator_info const & o) {
     out << pp(o);
     return out;
 }
+
+regular const & operator<<(regular const & out, operator_info const & o) {
+    out.m_io_state.get_regular_channel().get_stream() << mk_pair(pp(o), out.m_io_state.get_options());
+    return out;
+}
+
+diagnostic const & operator<<(diagnostic const & out, operator_info const & o) {
+    out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(pp(o), out.m_io_state.get_options());
+    return out;
+}
 }
diff --git a/src/frontends/lean/operator_info.h b/src/frontends/lean/operator_info.h
index 3daef1d30..712328e28 100644
--- a/src/frontends/lean/operator_info.h
+++ b/src/frontends/lean/operator_info.h
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/name.h"
 #include "util/list.h"
 #include "util/sexpr/format.h"
+#include "library/io_state.h"
 #include "kernel/object.h"
 
 namespace lean {
@@ -110,6 +111,9 @@ inline operator_info mixfixo(std::initializer_list<name> const & l, unsigned pre
 format pp(operator_info const & o);
 std::ostream & operator<<(std::ostream & out, operator_info const & o);
 
+regular const & operator<<(regular const & out, operator_info const & o);
+diagnostic const & operator<<(diagnostic const & out, operator_info const & o);
+
 /**
     \brief Create object for tracking notation/operator declarations.
     This object is mainly used for recording the declaration.