From b05b514cc2425a08a77c4c41ff4cc0bb1aabaabf Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 11 Oct 2016 17:29:01 -0400
Subject: [PATCH] refactor(*): structured message objects

---
 src/api/exception.cpp                         |  20 --
 src/api/ios.cpp                               |   4 +-
 src/frontends/lean/builtin_cmds.cpp           |  66 +++---
 src/frontends/lean/builtin_cmds.h             |   5 +-
 src/frontends/lean/decl_cmds.cpp              |   2 -
 src/frontends/lean/definition_cmds.cpp        |  41 ++--
 src/frontends/lean/elaborator.cpp             |   8 +-
 src/frontends/lean/parser.cpp                 |  89 +++-----
 src/frontends/lean/parser.h                   |  14 +-
 src/frontends/lean/pp.cpp                     |  36 ----
 src/frontends/lean/print_cmd.cpp              | 190 ++++++++----------
 src/frontends/smt2/parser.cpp                 |   8 +-
 src/library/CMakeLists.txt                    |   5 +-
 src/library/abstract_parser.h                 |   2 +
 src/library/error_handling.cpp                | 157 ---------------
 src/library/error_handling.h                  |  36 ----
 src/library/flycheck.cpp                      |  11 +-
 src/library/flycheck.h                        |  17 +-
 src/library/io_state.cpp                      |  12 +-
 src/library/io_state.h                        |   8 +
 src/library/io_state_stream.h                 |   9 +-
 src/library/message_builder.cpp               |  55 +++++
 src/library/message_builder.h                 |  55 +++++
 src/library/messages.cpp                      |  41 ++++
 src/library/messages.h                        |  58 ++++++
 src/shell/emscripten.cpp                      |  11 +-
 src/shell/lean.cpp                            |  31 +--
 src/util/exception.h                          |   1 +
 tests/lean/char_lits.lean.expected.out        |   5 +-
 .../lean/concrete_instance.lean.expected.out  |   8 +-
 tests/lean/elab_error_msgs.lean.expected.out  |   1 -
 .../lean/unification_hints1.lean.expected.out |  12 +-
 32 files changed, 434 insertions(+), 584 deletions(-)
 delete mode 100644 src/library/error_handling.cpp
 delete mode 100644 src/library/error_handling.h
 create mode 100644 src/library/message_builder.cpp
 create mode 100644 src/library/message_builder.h
 create mode 100644 src/library/messages.cpp
 create mode 100644 src/library/messages.h

diff --git a/src/api/exception.cpp b/src/api/exception.cpp
index 01cd5d1f44..12753c5b47 100644
--- a/src/api/exception.cpp
+++ b/src/api/exception.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/type_checker.h"
 #include "library/print.h"
-#include "library/error_handling.h"
 #include "api/exception.h"
 #include "api/string.h"
 using namespace lean; // NOLINT
@@ -41,25 +40,6 @@ char const * lean_exception_get_message(lean_exception e) {
     }
 }
 
-char const * lean_exception_get_detailed_message(lean_exception e) {
-    if (!e)
-        return 0;
-    try {
-        formatter_factory fmtf = mk_print_formatter_factory();
-        std::shared_ptr<output_channel> out(new string_output_channel());
-        io_state ios(fmtf);
-        ios.set_regular_channel(out);
-        ios.set_diagnostic_channel(out);
-        environment env;
-        type_checker tc(env);
-        io_state_stream ioss(env, ios, tc);
-        display_error(ioss, nullptr, *lean::to_exception(e));
-        return mk_string(static_cast<string_output_channel const *>(out.get())->str());
-    } catch (...) {
-        return 0;
-    }
-}
-
 lean_exception_kind lean_exception_get_kind(lean_exception e) {
     lean::throwable * ex = lean::to_exception(e);
     if (!ex)
diff --git a/src/api/ios.cpp b/src/api/ios.cpp
index 5c728f18fa..1aaf6327d7 100644
--- a/src/api/ios.cpp
+++ b/src/api/ios.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/error_handling.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/pp.h"
 #include "api/string.h"
 #include "api/exception.h"
@@ -116,7 +116,7 @@ lean_bool lean_exception_to_pp_string(lean_env env, lean_ios ios, lean_exception
     type_checker tc(to_env_ref(env));
     io_state_stream ioss(to_env_ref(env), new_ios, tc);
     throwable * _e = to_exception(e);
-    display_error(ioss, nullptr, *_e);
+    ioss << _e->what();
     *r = mk_string(static_cast<string_output_channel const *>(aux.get())->str());
     LEAN_CATCH;
 }
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index fd8545eb93..32fa164462 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -165,18 +165,14 @@ environment check_cmd(parser & p) {
     std::tie(e, ls) = parse_local_expr(p);
     type_checker tc(p.env(), true, false);
     expr type = tc.check(e, ls);
-    auto out              = regular(p.env(), p.ios(), tc);
+    auto out              = p.mk_message(p.cmd_pos(), INFORMATION);
     formatter fmt         = out.get_formatter();
     unsigned indent       = get_pp_indent(p.get_options());
     format e_fmt    = fmt(e);
     format type_fmt = fmt(type);
     format r = group(e_fmt + space() + colon() + nest(indent, line() + type_fmt));
-    flycheck_information info(p.ios());
-    if (info.enabled()) {
-        p.display_information_pos(p.cmd_pos());
-        out << "check result:\n";
-    }
-    out << mk_pair(r, p.get_options()) << endl;
+    out.set_caption("check result") << r;
+    out.report();
     return p.env();
 }
 
@@ -197,21 +193,14 @@ environment eval_cmd(parser & p) {
         bool eta = false;
         r = normalize(tc, e, eta);
     }
-    flycheck_information info(p.ios());
-    if (info.enabled()) {
-        p.display_information_pos(p.cmd_pos());
-        p.ios().get_regular_stream() << "eval result:\n";
-    }
-    type_context tc(p.env(), p.get_options());
-    auto out = regular(p.env(), p.ios(), tc);
-    out << r << endl;
+    auto out = p.mk_message(p.cmd_pos(), INFORMATION);
+    out.set_caption("eval result") << r;
+    out.report();
     return p.env();
 }
 
 environment exit_cmd(parser & p) {
-    flycheck_warning wrn(p.ios());
-    p.display_warning_pos(p.cmd_pos());
-    p.ios().get_regular_stream() << " using 'exit' to interrupt Lean" << std::endl;
+    (p.mk_message(p.cmd_pos(), WARNING) << "using 'exit' to interrupt Lean").report();
     throw interrupt_parser();
 }
 
@@ -337,18 +326,13 @@ static environment local_cmd(parser & p) {
 }
 
 static environment help_cmd(parser & p) {
-    flycheck_information info(p.ios());
-    if (info.enabled()) {
-        p.display_information_pos(p.cmd_pos());
-        p.ios().get_regular_stream() << "help result:\n";
-    }
+    auto rep = p.mk_message(p.cmd_pos(), INFORMATION);
     if (p.curr_is_token_or_id(get_options_tk())) {
         p.next();
         auto decls = get_option_declarations();
         decls.for_each([&](name const &, option_declaration const & opt) {
-                p.ios().get_regular_stream()
-                    << "  " << opt.get_name() << " (" << opt.kind() << ") "
-                    << opt.get_description() << " (default: " << opt.get_default_value() << ")" << std::endl;
+                rep << "  " << opt.get_name() << " (" << opt.kind() << ") "
+                    << opt.get_description() << " (default: " << opt.get_default_value() << ")\n";
             });
     } else if (p.curr_is_token_or_id(get_commands_tk())) {
         p.next();
@@ -359,14 +343,13 @@ static environment help_cmd(parser & p) {
             });
         std::sort(ns.begin(), ns.end());
         for (name const & n : ns) {
-            p.ios().get_regular_stream()
-                << "  " << n << ": " << cmds.find(n)->get_descr() << std::endl;
+            rep << "  " << n << ": " << cmds.find(n)->get_descr() << "\n";
         };
     } else {
-        p.ios().get_regular_stream()
-            << "help options  : describe available options\n"
+        rep << "help options  : describe available options\n"
             << "help commands : describe available commands\n";
     }
+    rep.report();
     return p.env();
 }
 
@@ -409,16 +392,14 @@ static environment unify_cmd(parser & p) {
     local_context   lctx;
     e1 = convert_metavars(mctx, e1);
     e2 = convert_metavars(mctx, e2);
-    tout() << e1 << " =?= " << e2 << "\n";
+    auto rep = p.mk_message(p.cmd_pos(), INFORMATION);
+    rep << e1 << " =?= " << e2 << "\n";
     type_context ctx(env, p.get_options(), mctx, lctx, transparency_mode::Semireducible);
     bool success = ctx.is_def_eq(e1, e2);
     if (success)
-        tout() << ctx.instantiate_mvars(e1) << " =?= " << ctx.instantiate_mvars(e2) << "\n";
-    flycheck_information info(p.ios());
-    if (info.enabled()) {
-        p.display_information_pos(p.cmd_pos());
-    }
-    p.ios().get_regular_stream() << (success ? "success" : "fail") << std::endl;
+        rep << ctx.instantiate_mvars(e1) << " =?= " << ctx.instantiate_mvars(e2) << "\n";
+    rep << (success ? "unification successful" : "unification failed");
+    rep.report();
     return env;
 }
 
@@ -483,8 +464,11 @@ static environment vm_eval_cmd(parser & p) {
     vm_state s(new_env);
     optional<vm_obj> initial_state;
     if (is_IO) initial_state = mk_vm_simple(0);
+    auto out = p.mk_message(INFORMATION);
+    out.set_caption("vm_eval result");
+    // TODO(gabriel): capture output
     if (p.profiling()) {
-        timeit timer(p.ios().get_diagnostic_stream(), "vm_eval time");
+        timeit timer(out.get_text_stream().get_stream(), "vm_eval time");
         vm_eval_core(s, main, initial_state);
     } else {
         vm_eval_core(s, main, initial_state);
@@ -493,13 +477,13 @@ static environment vm_eval_cmd(parser & p) {
         // do not print anything
     } else if (is_string) {
         vm_obj r = s.get(0);
-        p.ios().get_regular_stream() << to_string(r) << "\n";
+        out << to_string(r);
     } else {
         /* if it is not IO nor a string, then display object on top of the stack using vm_obj display method */
         vm_obj r = s.get(0);
-        display(p.ios().get_regular_stream(), r);
-        p.ios().get_regular_stream() << "\n";
+        display(out.get_text_stream().get_stream(), r);
     }
+    out.report();
     return p.env();
 }
 
diff --git a/src/frontends/lean/builtin_cmds.h b/src/frontends/lean/builtin_cmds.h
index 1d7135c451..87430cc0d4 100644
--- a/src/frontends/lean/builtin_cmds.h
+++ b/src/frontends/lean/builtin_cmds.h
@@ -6,9 +6,10 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "frontends/lean/cmd_table.h"
+#include "library/message_builder.h"
 namespace lean {
-bool print_id_info(parser & p, name const & id, bool show_value, pos_info const & pos);
-bool print_token_info(parser const & p, name const & tk);
+bool print_id_info(parser & p, message_builder & out, name const & id, bool show_value, pos_info const & pos);
+bool print_token_info(parser const & p, message_builder & out, name const & tk);
 
 cmd_table get_builtin_cmds();
 /* \brief Replay export declarations in the top-level of imported files */
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 6a960deeff..52559ea830 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -22,8 +22,6 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/explicit.h"
 #include "library/unfold_macros.h"
-#include "library/flycheck.h"
-#include "library/error_handling.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/util.h"
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index f1f7448288..2b37a0d6c3 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -20,7 +20,6 @@ Author: Leonardo de Moura
 #include "library/noncomputable.h"
 #include "library/module.h"
 #include "library/flycheck.h"
-#include "library/error_handling.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/replace_visitor.h"
 #include "library/equations_compiler/equations.h"
@@ -218,17 +217,15 @@ static expr_pair elaborate_definition_core(elaborator & elab, def_cmd_kind kind,
     }
 }
 
-static void display_pos(std::ostream & out, parser const & p, pos_info const & pos) {
-    display_pos(out, p.get_stream_name().c_str(), pos.first, pos.second);
-}
-
 static expr_pair elaborate_definition(parser & p, elaborator & elab, def_cmd_kind kind, expr const & fn, expr const & val, pos_info const & pos) {
     if (p.profiling()) {
-        std::ostringstream msg;
-        display_pos(msg, p, pos);
-        msg << " elaboration time for " << local_pp_name(fn);
-        timeit timer(p.ios().get_diagnostic_stream(), msg.str().c_str(), LEAN_PROFILE_THRESHOLD);
-        return elaborate_definition_core(elab, kind, fn, val);
+        auto msg = p.mk_message(pos, INFORMATION);
+        msg << "elaboration time for " << fn;
+        {
+            timeit timer(msg.get_text_stream().get_stream(), "", LEAN_PROFILE_THRESHOLD);
+            return elaborate_definition_core(elab, kind, fn, val);
+        }
+        msg.report();
     } else {
         return elaborate_definition_core(elab, kind, fn, val);
     }
@@ -264,11 +261,13 @@ static pair<environment, name> mk_real_name(environment const & env, name const
 
 static certified_declaration check(parser & p, environment const & env, name const & c_name, declaration const & d, pos_info const & pos) {
     if (p.profiling()) {
-        std::ostringstream msg;
-        display_pos(msg, p, pos);
-        msg << " type checking time for " << c_name;
-        timeit timer(p.ios().get_diagnostic_stream(), msg.str().c_str(), LEAN_PROFILE_THRESHOLD);
-        return ::lean::check(env, d);
+        auto msg = p.mk_message(pos, INFORMATION);
+        msg << "type checking time for " << c_name;
+        {
+            timeit timer(msg.get_text_stream().get_stream(), "", LEAN_PROFILE_THRESHOLD);
+            return ::lean::check(env, d);
+        }
+        msg.report();
     } else {
         return ::lean::check(env, d);
     }
@@ -297,13 +296,11 @@ static environment compile_decl(parser & p, environment const & env, def_cmd_kin
     } catch (exception & ex) {
         if (p.found_errors())
             return env;
-        flycheck_warning wrn(p.ios());
-        auto & out = p.ios().get_regular_stream();
-        display_pos(out, p, pos);
-        out << "failed to generate bytecode for '" << c_name << "'" << std::endl;
-        type_context ctx(p.env());
-        auto out2  = regular(p.env(), p.ios(), ctx);
-        display_warning(out2, get_pos_info_provider(), ex);
+        // FIXME(gabriel): use position from exception
+        auto out = p.mk_message(pos, WARNING);
+        out << "failed to generate bytecode for '" << c_name << "'\n";
+        out.set_exception(ex);
+        out.report();
         return env;
     }
 }
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index e2441de190..df30d3b977 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -28,7 +28,6 @@ Author: Leonardo de Moura
 #include "library/pp_options.h"
 #include "library/flycheck.h"
 #include "library/replace_visitor.h"
-#include "library/error_handling.h"
 #include "library/locals.h"
 #include "library/private.h"
 #include "library/attribute_manager.h"
@@ -2289,11 +2288,8 @@ void elaborator::show_goal(tactic_state const & s, expr const & start_ref, expr
     if (curr_pos->first < line || (curr_pos->first == line && curr_pos->second < col))
         return;
     m_show_goal_pos = optional<pos_info>();
-    auto out = regular(m_env, get_global_ios(), m_ctx);
-    print_lean_info_header(out.get_stream());
-    out << "position " << curr_pos->first << ":" << curr_pos->second << "\n";
-    out << s.pp(get_global_ios().get_formatter_factory()) << "\n";
-    print_lean_info_footer(out.get_stream());
+    get_global_ios().report(message(provider->get_file_name(), *curr_pos, INFORMATION,
+        (sstream() << mk_pair(s.pp(get_global_ios().get_formatter_factory()), get_global_ios().get_options())).str()));
 }
 
 /* Apply the given tactic to the state 's'.
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index b3379258c3..7088866459 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -43,7 +43,6 @@ Author: Leonardo de Moura
 #include "library/flycheck.h"
 #include "library/pp_options.h"
 #include "library/noncomputable.h"
-#include "library/error_handling.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/type_context.h"
 #include "library/equations_compiler/equations.h"
@@ -216,35 +215,33 @@ void parser::scan() {
             if (curr_is_identifier()) {
                 name const & id = get_name_val();
                 if (p.second <= m_info_at_col && m_info_at_col < p.second + id.utf8_size()) {
-                    print_lean_info_header(m_ios.get_regular_stream());
+                    auto out = mk_message(INFORMATION);
                     bool ok = true;
                     try {
                         bool show_value = false;
-                        ok = print_id_info(*this, id, show_value, p);
+                        ok = print_id_info(*this, out, id, show_value, p);
                     } catch (exception &) {
                         ok = false;
                     }
                     if (!ok)
-                        m_ios.get_regular_stream() << "unknown identifier '" << id << "'\n";
-                    print_lean_info_footer(m_ios.get_regular_stream());
+                        out << "unknown identifier '" << id << "'\n";
+                    out.report();
                     m_info_at = false;
                 }
             } else if (curr_is_keyword()) {
                 name const & tk = get_token_info().token();
                 if (p.second <= m_info_at_col && m_info_at_col < p.second + tk.utf8_size()) {
-                    print_lean_info_header(m_ios.get_regular_stream());
+                    auto out = mk_message(INFORMATION);
                     try {
-                        print_token_info(*this, tk);
+                        print_token_info(*this, out, tk);
                     } catch (exception &) {}
-                    print_lean_info_footer(m_ios.get_regular_stream());
+                    out.report();
                     m_info_at = false;
                 }
             } else if (curr_is_command()) {
                 name const & tk = get_token_info().token();
                 if (p.second <= m_info_at_col && m_info_at_col < p.second + tk.utf8_size()) {
-                    print_lean_info_header(m_ios.get_regular_stream());
-                    m_ios.get_regular_stream() << "'" << tk << "' is a command\n";
-                    print_lean_info_footer(m_ios.get_regular_stream());
+                    (mk_message(INFORMATION) << "'" << tk << "' is a command").report();
                     m_info_at = false;
                 }
             }
@@ -284,9 +281,7 @@ expr parser::mk_sorry(pos_info const & p) {
         // TODO(Leo): remove the #ifdef.
         // The compilation option LEAN_IGNORE_SORRY is a temporary hack for the nightly builds
         // We use it to avoid a buch of warnings on cdash.
-        flycheck_warning wrn(m_ios);
-        display_warning_pos(p.first, p.second);
-        m_ios.get_regular_stream() << " using 'sorry'" << std::endl;
+        (mk_message(p, WARNING) << "using 'sorry'").report();
 #endif
     }
     return save_pos(::lean::mk_sorry(), p);
@@ -308,38 +303,6 @@ void parser::updt_options() {
     }
 }
 
-void parser::display_warning_pos(unsigned line, unsigned pos) {
-    type_context tc(env(), get_options());
-    auto out = regular(env(), ios(), tc);
-    ::lean::display_warning_pos(out, get_stream_name().c_str(), line, pos);
-}
-void parser::display_warning_pos(pos_info p) { display_warning_pos(p.first, p.second); }
-
-void parser::display_information_pos(pos_info pos) {
-    ::lean::display_information_pos(ios().get_regular_stream(), get_options(),
-                                    get_stream_name().c_str(), pos.first, pos.second);
-}
-
-void parser::display_error_pos(unsigned line, unsigned pos) {
-    ::lean::display_error_pos(ios().get_regular_stream(), get_options(),
-                              get_stream_name().c_str(), line, pos);
-}
-void parser::display_error_pos(pos_info p) { display_error_pos(p.first, p.second); }
-
-void parser::display_error(char const * msg, unsigned line, unsigned pos) {
-    flycheck_error err(ios());
-    display_error_pos(line, pos);
-    ios().get_regular_stream() << " " << msg << std::endl;
-}
-
-void parser::display_error(char const * msg, pos_info p) { display_error(msg, p.first, p.second); }
-
-void parser::display_error(throwable const & ex) {
-    type_context tc(env(), get_options());
-    auto out = regular(env(), ios(), tc);
-    ::lean::display_error(out, this, ex);
-}
-
 void parser::throw_parser_exception(char const * msg, pos_info p) {
     throw parser_exception(msg, get_stream_name().c_str(), p.first, p.second);
 }
@@ -364,21 +327,21 @@ void parser::protected_call(std::function<void()> && f, std::function<void()> &&
             ex.get_exception().rethrow();
         }
     } catch (parser_exception & ex) {
-        CATCH(flycheck_error err(ios()); ios().get_regular_stream() << ex.what() << std::endl,
-              throw);
+        CATCH(ios().report(ex), throw);
     } catch (parser_error & ex) {
-        CATCH(display_error(ex.what(), ex.m_pos),
+        CATCH((mk_message(ex.m_pos, ERROR) << ex.get_msg()).report(),
               throw_parser_exception(ex.what(), ex.m_pos));
     } catch (interrupted & ex) {
         reset_interrupt();
         if (m_verbose)
-            ios().get_regular_stream() << "!!!Interrupted!!!" << std::endl;
+            (mk_message(m_last_cmd_pos, ERROR) << "!!!Interrupted!!!").report();
         sync();
         if (m_use_exceptions)
             throw;
     } catch (throwable & ex) {
         reset_interrupt();
-        CATCH(display_error(ex), throw_nested_exception(ex, m_last_cmd_pos));
+        CATCH(mk_message(m_last_cmd_pos, ERROR).set_exception(ex).report(),
+              throw_nested_exception(ex, m_last_cmd_pos));
     }
 }
 
@@ -2108,13 +2071,11 @@ void parser::parse_imports() {
             olean_files.push_back(module_name(k, f));
         } else {
             m_found_errors = true;
-            if (!m_use_exceptions && m_show_errors) {
-                flycheck_error err(ios());
-                display_error_pos(pos());
-                ios().get_regular_stream() << " invalid import, unknown module '" << f << "'" << std::endl;
-            }
+            parser_error error(sstream() << "invalid import, unknown module '" << f << "'", pos());
+            if (!m_use_exceptions && m_show_errors)
+                ios().report(message(get_file_name(), error.m_pos, ERROR, error.get_msg()));
             if (m_use_exceptions)
-                throw parser_error(sstream() << "invalid import, unknown module '" << f << "'", pos());
+                throw error;
         }
     };
     if (!prelude) {
@@ -2182,9 +2143,7 @@ bool parser::parse_commands() {
             // TODO(Leo): remove the #ifdef.
             // The compilation option LEAN_IGNORE_SORRY is a temporary hack for the nightly builds
             // We use it to avoid a buch of warnings on cdash.
-            flycheck_warning wrn(ios());
-            display_warning_pos(pos());
-            ios().get_regular_stream() << " imported file uses 'sorry'" << std::endl;
+            (mk_message(WARNING) << "imported file uses 'sorry'").report();
 #endif
         }
         while (!done) {
@@ -2217,7 +2176,7 @@ bool parser::parse_commands() {
         if (has_open_scopes(m_env)) {
             m_found_errors = true;
             if (!m_use_exceptions && m_show_errors)
-                display_error("invalid end of module, expecting 'end'", pos());
+                (mk_message(ERROR) << "invalid end of module, expecting 'end'").report();
             else if (m_use_exceptions)
                 throw_parser_exception("invalid end of module, expecting 'end'", pos());
         }
@@ -2291,6 +2250,14 @@ char const * parser::get_file_name() const {
     return get_stream_name().c_str();
 }
 
+message_builder parser::mk_message(pos_info const &p, message_severity severity) {
+    std::shared_ptr<abstract_type_context> tc = std::make_shared<type_context>(env(), get_options());
+    return message_builder(this, tc, env(), ios(), get_file_name(), p, severity);
+}
+message_builder parser::mk_message(message_severity severity) {
+    return mk_message(pos(), severity);
+}
+
 bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name,
                     optional<std::string> const & base_dir, bool use_exceptions,
                     unsigned num_threads, definition_cache * cache) {
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 83b645f71d..a785920971 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "library/abstract_parser.h"
 #include "library/io_state.h"
 #include "library/io_state_stream.h"
+#include "library/message_builder.h"
 #include "library/definition_cache.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/local_decls.h"
@@ -135,11 +136,6 @@ class parser : public abstract_parser {
     // noncomputable definitions not tagged as noncomputable.
     bool                   m_ignore_noncomputable;
 
-    void display_warning_pos(unsigned line, unsigned pos);
-    void display_error_pos(unsigned line, unsigned pos);
-    void display_error_pos(pos_info p);
-    void display_error(char const * msg, unsigned line, unsigned pos);
-    void display_error(char const * msg, pos_info p);
     void throw_parser_exception(char const * msg, pos_info p);
     void throw_nested_exception(throwable const & ex, pos_info p);
 
@@ -213,8 +209,6 @@ public:
            snapshot const * s = nullptr, snapshot_vector * sv = nullptr);
     ~parser();
 
-    void display_error(throwable const & ex);
-
     bool ignore_noncomputable() const { return m_ignore_noncomputable; }
     void set_ignore_noncomputable() { m_ignore_noncomputable = true; }
 
@@ -240,6 +234,9 @@ public:
     environment const & env() const { return m_env; }
     io_state const & ios() const { return m_ios; }
 
+    message_builder mk_message(pos_info const & p, message_severity severity);
+    message_builder mk_message(message_severity severity);
+
     local_level_decls const & get_local_level_decls() const { return m_local_level_decls; }
     local_expr_decls const & get_local_expr_decls() const { return m_local_decls; }
 
@@ -479,9 +476,6 @@ public:
     expr mk_sorry(pos_info const & p);
     bool used_sorry() const { return m_used_sorry; }
 
-    void display_information_pos(pos_info p);
-    void display_warning_pos(pos_info p);
-
     /** return true iff profiling is enabled */
     bool profiling() const { return m_profile; }
 
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index d9b356c40b..982ea953cc 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1731,40 +1731,4 @@ formatter_factory mk_pretty_formatter_factory() {
     };
 }
 
-static options mk_options(bool detail) {
-    options opts;
-    if (detail) {
-        opts = opts.update(name{"pp", "implicit"}, true);
-        opts = opts.update(name{"pp", "notation"}, false);
-    }
-    return opts;
 }
-
-static void pp_core(environment const & env, expr const & e, bool detail) {
-    type_checker tc(env);
-    io_state ios(mk_pretty_formatter_factory(), mk_options(detail));
-    regular(env, ios, tc) << e << "\n";
-}
-
-/* static void pp_core(environment const & env, goal const & g, bool detail) {
-    type_checker tc(env);
-    io_state ios(mk_pretty_formatter_factory(), mk_options(detail));
-    regular(env, ios, tc) << g << "\n";
-}
-
-static void pp_core(environment const & env, proof_state const & s, bool detail) {
-    type_checker tc(env);
-    io_state ios(mk_pretty_formatter_factory(), mk_options(detail));
-    auto out = regular(env, ios, tc);
-    out << s.pp(out.get_formatter()) << "\n";
-}
-*/
-
-}
-// for debugging purposes
-void pp(lean::environment const & env, lean::expr const & e) { lean::pp_core(env, e, false); }
-// void pp(lean::environment const & env, lean::goal const & g) { lean::pp_core(env, g, false); }
-// void pp(lean::environment const & env, lean::proof_state const & s) { lean::pp_core(env, s, false); }
-void pp_detail(lean::environment const & env, lean::expr const & e) { lean::pp_core(env, e, true); }
-// void pp_detail(lean::environment const & env, lean::goal const & g) { lean::pp_core(env, g, true); }
-// void pp_detail(lean::environment const & env, lean::proof_state const & s) { lean::pp_core(env, s, true); }
diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp
index f7c9f62e84..f5d7f2cf0f 100644
--- a/src/frontends/lean/print_cmd.cpp
+++ b/src/frontends/lean/print_cmd.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include <string>
+#include <library/trace.h>
 #include "util/sstream.h"
 #include "util/sexpr/option_declarations.h"
 #include "kernel/for_each_fn.h"
@@ -14,7 +15,6 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/class.h"
 #include "library/aliases.h"
-#include "library/flycheck.h"
 #include "library/pp_options.h"
 #include "library/private.h"
 #include "library/protected.h"
@@ -69,22 +69,19 @@ struct print_axioms_deps {
     }
 };
 
-static environment print_axioms(parser & p) {
+static environment print_axioms(parser & p, message_builder & out) {
     if (p.curr_is_identifier()) {
         name c = p.check_constant_next("invalid 'print axioms', constant expected");
         environment new_env = p.reveal_all_theorems();
         type_context tc(new_env, p.get_options());
-        auto out = regular(new_env, p.ios(), tc);
-        print_axioms_deps(p.env(), out)(c);
+        auto new_out = io_state_stream(new_env, p.ios(), tc, out.get_text_stream().get_channel());
+        print_axioms_deps(p.env(), new_out)(c);
         return new_env;
     } else {
         bool has_axioms = false;
-        environment const & env = p.env();
-        type_context tc(env, p.get_options());
-        auto out = regular(env, p.ios(), tc);
-        env.for_each_declaration([&](declaration const & d) {
+        p.env().for_each_declaration([&](declaration const & d) {
                 name const & n = d.get_name();
-                if (!d.is_definition() && !env.is_builtin(n) && d.is_trusted()) {
+                if (!d.is_definition() && !p.env().is_builtin(n) && d.is_trusted()) {
                     out << n << " : " << d.get_type() << endl;
                     has_axioms = true;
                 }
@@ -95,33 +92,28 @@ static environment print_axioms(parser & p) {
     }
 }
 
-static void print_prefix(parser & p) {
+static void print_prefix(parser & p, message_builder & out) {
     name prefix = p.check_id_next("invalid 'print prefix' command, identifier expected");
-    environment const & env = p.env();
     buffer<declaration> to_print;
-    type_context tc(env, p.get_options());
-    auto out = regular(env, p.ios(), tc);
-    env.for_each_declaration([&](declaration const & d) {
+    p.env().for_each_declaration([&](declaration const & d) {
             if (is_prefix_of(prefix, d.get_name())) {
                 to_print.push_back(d);
             }
         });
     std::sort(to_print.begin(), to_print.end(), [](declaration const & d1, declaration const & d2) { return d1.get_name() < d2.get_name(); });
     for (declaration const & d : to_print) {
-        out << d.get_name() << " : " << d.get_type() << endl;
+        out << d.get_name() << " : " << d.get_type() << "\n";
     }
     if (to_print.empty())
-        out << "no declaration starting with prefix '" << prefix << "'" << endl;
+        out << "no declaration starting with prefix '" << prefix << "'\n";
 }
 
-static void print_fields(parser const & p, name const & S, pos_info const & pos) {
+static void print_fields(parser const & p, message_builder & out, name const & S, pos_info const & pos) {
     environment const & env = p.env();
     if (!is_structure(env, S))
         throw parser_error(sstream() << "invalid 'print fields' command, '" << S << "' is not a structure", pos);
     buffer<name> field_names;
     get_structure_fields(env, S, field_names);
-    type_context tc(env, p.get_options());
-    auto out = regular(env, p.ios(), tc);
     for (name const & field_name : field_names) {
         declaration d = env.get(field_name);
         out << d.get_name() << " : " << d.get_type() << endl;
@@ -142,16 +134,13 @@ static bool uses_some_token(unsigned num, notation::transition const * ts, buffe
         std::any_of(tokens.begin(), tokens.end(), [&](name const & token) { return uses_token(num, ts, token); });
 }
 
-static bool print_parse_table(parser const & p, parse_table const & t, bool nud, buffer<name> const & tokens, bool tactic_table = false) {
+static bool print_parse_table(parser const & p, message_builder & rep, parse_table const & t, bool nud, buffer<name> const & tokens, bool tactic_table = false) {
     bool found = false;
-    io_state ios = p.ios();
-    options os   = ios.get_options();
+    options os   = rep.get_text_stream().get_options();
     os = os.update_if_undef(get_pp_full_names_name(), true);
     os = os.update(get_pp_notation_name(), false);
     os = os.update(get_pp_preterm_name(), true);
-    ios.set_options(os);
-    type_context tc(p.env(), p.get_options());
-    io_state_stream out = regular(p.env(), ios, tc);
+    auto out = rep.get_text_stream().update_options(os);
     optional<token_table> tt(get_token_table(p.env()));
     t.for_each([&](unsigned num, notation::transition const * ts, list<notation::accepting> const & overloads) {
             if (uses_some_token(num, ts, tokens)) {
@@ -164,19 +153,19 @@ static bool print_parse_table(parser const & p, parse_table const & t, bool nud,
     return found;
 }
 
-static void print_notation(parser & p) {
+static void print_notation(parser & p, message_builder & out) {
     buffer<name> tokens;
     while (p.curr_is_keyword()) {
         tokens.push_back(p.get_token_info().token());
         p.next();
     }
     bool found = false;
-    if (print_parse_table(p, get_nud_table(p.env()), true, tokens))
+    if (print_parse_table(p, out, get_nud_table(p.env()), true, tokens))
         found = true;
-    if (print_parse_table(p, get_led_table(p.env()), false, tokens))
+    if (print_parse_table(p, out, get_led_table(p.env()), false, tokens))
         found = true;
     if (!found)
-        p.ios().get_regular_stream() << "no notation" << std::endl;
+        out << "no notation";
 }
 
 #if 0
@@ -225,25 +214,21 @@ static name to_user_name(environment const & env, name const & n) {
         return n;
 }
 
-static void print_definition(parser const & p, name const & n, pos_info const & pos) {
+static void print_definition(parser const & p, message_builder & out, name const & n, pos_info const & pos) {
     environment const & env = p.env();
     declaration d = env.get(n);
-    options opts        = p.get_options();
-    opts                = opts.update_if_undef(get_pp_beta_name(), false);
-    io_state ios(p.ios(), opts);
-    type_context tc(env, opts);
-    io_state_stream out = regular(env, ios, tc);
     if (d.is_axiom())
         throw parser_error(sstream() << "invalid 'print definition', theorem '" << to_user_name(env, n)
                            << "' is not available (suggestion: use command 'reveal " << to_user_name(env, n) << "')", pos);
     if (!d.is_definition())
         throw parser_error(sstream() << "invalid 'print definition', '" << to_user_name(env, n) << "' is not a definition", pos);
-    out << d.get_value() << endl;
+    options opts        = out.get_text_stream().get_options();
+    opts                = opts.update_if_undef(get_pp_beta_name(), false);
+    out.get_text_stream().update_options(opts) << d.get_value() << endl;
 }
 
-static void print_attributes(parser const & p, name const & n) {
+static void print_attributes(parser const & p, message_builder & out, name const & n) {
     environment const & env = p.env();
-    std::ostream & out = p.ios().get_regular_stream();
     buffer<attribute const *> attrs;
     get_attributes(p.env(), attrs);
     std::sort(attrs.begin(), attrs.end(), [](attribute const * a1, attribute const * a2) {
@@ -261,7 +246,7 @@ static void print_attributes(parser const & p, name const & n) {
                 out << ", ";
             }
             out << attr->get_name();
-            data->print(out);
+            data->print(out.get_text_stream().get_stream());
             unsigned prio = attr->get_prio(env, n);
             if (prio != LEAN_DEFAULT_PRIORITY)
                 out << ", priority " << prio;
@@ -271,13 +256,11 @@ static void print_attributes(parser const & p, name const & n) {
         out << "]\n";
 }
 
-static void print_inductive(parser const & p, name const & n, pos_info const & pos) {
+static void print_inductive(parser const & p, message_builder & out, name const & n, pos_info const & pos) {
     environment const & env = p.env();
-    type_checker tc(env);
-    io_state_stream out = regular(env, p.ios(), tc);
     if (auto idecl = inductive::is_inductive_decl(env, n)) {
         level_param_names ls = idecl->m_level_params;
-        print_attributes(p, n);
+        print_attributes(p, out, n);
         if (is_structure(env, n))
             out << "structure";
         else
@@ -286,7 +269,7 @@ static void print_inductive(parser const & p, name const & n, pos_info const & p
         out << " : " << env.get(n).get_type() << "\n";
         if (is_structure(env, n)) {
             out << "fields:\n";
-            print_fields(p, n, pos);
+            print_fields(p, out, n, pos);
         } else {
             out << "constructors:\n";
             buffer<name> constructors;
@@ -300,9 +283,8 @@ static void print_inductive(parser const & p, name const & n, pos_info const & p
     }
 }
 
-static void print_recursor_info(parser & p) {
+static void print_recursor_info(parser & p, message_builder & out) {
     name c = p.check_constant_next("invalid 'print [recursor]', constant expected");
-    std::ostream & out = p.ios().get_regular_stream();
     recursor_info info = get_recursor_info(p.env(), c);
     out << "recursor information\n"
         << "  num. parameters:          " << info.get_num_params() << "\n"
@@ -339,28 +321,26 @@ static void print_recursor_info(parser & p) {
     }
 }
 
-static bool print_constant(parser const & p, char const * kind, declaration const & d, bool is_def = false) {
+static bool print_constant(parser const & p, message_builder & out, char const * kind, declaration const & d, bool is_def = false) {
     type_checker tc(p.env());
-    auto out = regular(p.env(), p.ios(), tc);
-    print_attributes(p, d.get_name());
+    print_attributes(p, out, d.get_name());
     if (is_protected(p.env(), d.get_name()))
         out << "protected ";
     if (d.is_definition() && is_marked_noncomputable(p.env(), d.get_name()))
         out << "noncomputable ";
     out << kind << " " << to_user_name(p.env(), d.get_name());
-    out.update_options(out.get_options().update((name {"pp", "binder_types"}), true)) << " : " << d.get_type();
+    out.get_text_stream().update_options(out.get_text_stream().get_options().update((name {"pp", "binder_types"}), true))
+            << " : " << d.get_type();
     if (is_def)
         out << " :=";
     out << "\n";
     return true;
 }
 
-bool print_id_info(parser & p, name const & id, bool show_value, pos_info const & pos) {
+bool print_id_info(parser & p, message_builder & out, name const & id, bool show_value, pos_info const & pos) {
     // declarations
     try {
         environment const & env = p.env();
-        type_checker tc(env);
-        auto out = regular(env, p.ios(), tc);
         try {
             list<name> cs = p.to_constants(id, "", pos);
             bool first = true;
@@ -368,27 +348,27 @@ bool print_id_info(parser & p, name const & id, bool show_value, pos_info const
                 if (first) first = false; else out << "\n";
                 declaration const & d = env.get(c);
                 if (d.is_theorem()) {
-                    print_constant(p, "theorem", d, show_value);
+                    print_constant(p, out, "theorem", d, show_value);
                     if (show_value)
-                        print_definition(p, c, pos);
+                        print_definition(p, out, c, pos);
                 } else if (d.is_axiom() || d.is_constant_assumption()) {
                     if (inductive::is_inductive_decl(env, c)) {
-                        print_inductive(p, c, pos);
+                        print_inductive(p, out, c, pos);
                     } else if (inductive::is_intro_rule(env, c)) {
-                        print_constant(p, "constructor", d);
+                        print_constant(p, out, "constructor", d);
                     } else if (inductive::is_elim_rule(env, c)) {
-                        print_constant(p, "eliminator", d);
+                        print_constant(p, out, "eliminator", d);
                     } else if (is_quotient_decl(env, c)) {
-                        print_constant(p, "builtin-quotient-type-constant", d);
+                        print_constant(p, out, "builtin-quotient-type-constant", d);
                     } else if (d.is_axiom()) {
-                        print_constant(p, "axiom", d);
+                        print_constant(p, out, "axiom", d);
                     } else {
-                        print_constant(p, "constant", d);
+                        print_constant(p, out, "constant", d);
                     }
                 } else if (d.is_definition()) {
-                    print_constant(p, "definition", d, show_value);
+                    print_constant(p, out, "definition", d, show_value);
                     if (show_value)
-                        print_definition(p, c, pos);
+                        print_definition(p, out, c, pos);
                 }
                 // print_patterns(p, c);
             }
@@ -423,32 +403,32 @@ bool print_id_info(parser & p, name const & id, bool show_value, pos_info const
     return false;
 }
 
-bool print_token_info(parser const & p, name const & tk) {
+bool print_token_info(parser const & p, message_builder & out, name const & tk) {
     buffer<name> tokens;
     tokens.push_back(tk);
     bool found = false;
-    if (print_parse_table(p, get_nud_table(p.env()), true, tokens)) {
+    if (print_parse_table(p, out, get_nud_table(p.env()), true, tokens)) {
         found = true;
     }
-    if (print_parse_table(p, get_led_table(p.env()), false, tokens)) {
+    if (print_parse_table(p, out, get_led_table(p.env()), false, tokens)) {
         found = true;
     }
     return found;
 }
 
-bool print_polymorphic(parser & p) {
+bool print_polymorphic(parser & p, message_builder & out) {
     auto pos = p.pos();
     try {
         name id = p.check_id_next("");
         bool show_value = true;
-        if (print_id_info(p, id, show_value, pos))
+        if (print_id_info(p, out, id, show_value, pos))
             return true;
     } catch (exception &) {}
 
     // notation
     if (p.curr_is_keyword()) {
         name tk = p.get_token_info().token();
-        if (print_token_info(p, tk)) {
+        if (print_token_info(p, out, tk)) {
             p.next();
             return true;
         }
@@ -456,30 +436,23 @@ bool print_polymorphic(parser & p) {
     return false;
 }
 
-static void print_unification_hints(parser & p) {
-    type_checker tc(p.env());
-    auto out = regular(p.env(), p.ios(), tc);
+static void print_unification_hints(parser & p, message_builder & out) {
     out << pp_unification_hints(get_unification_hints(p.env()), out.get_formatter());
 }
 
-static void print_simp_rules(parser & p) {
+static void print_simp_rules(parser & p, message_builder & out) {
     name attr = p.check_id_next("invalid 'print [simp]' command, identifier expected");
     simp_lemmas slss = get_simp_lemmas(p.env(), transparency_mode::Reducible, attr);
-    type_checker tc(p.env());
-    auto out = regular(p.env(), p.ios(), tc);
     out << slss.pp_simp(out.get_formatter());
 }
 
-static void print_congr_rules(parser & p) {
+static void print_congr_rules(parser & p, message_builder & out) {
     name attr = p.check_id_next("invalid 'print [congr]' command, identifier expected");
     simp_lemmas slss = get_simp_lemmas(p.env(), transparency_mode::Reducible, attr);
-    type_checker tc(p.env());
-    auto out = regular(p.env(), p.ios(), tc);
     out << slss.pp_congr(out.get_formatter());
 }
 
-static void print_aliases(parser const & p) {
-    std::ostream & out = p.ios().get_regular_stream();
+static void print_aliases(parser const & p, message_builder & out) {
     for_each_expr_alias(p.env(), [&](name const & n, list<name> const & as) {
             out << n << " -> {";
             bool first = true;
@@ -491,8 +464,7 @@ static void print_aliases(parser const & p) {
         });
 }
 
-static void print_key_equivalences(parser & p) {
-    std::ostream & out = p.ios().get_regular_stream();
+static void print_key_equivalences(parser & p, message_builder & out) {
     for_each_key_equivalence(p.env(), [&](buffer<name> const & ns) {
             out << "[";
             for (unsigned i = 0; i < ns.size(); i++) {
@@ -503,7 +475,7 @@ static void print_key_equivalences(parser & p) {
         });
 }
 
-static void print_attribute(parser & p, attribute const & attr) {
+static void print_attribute(parser & p, message_builder & out, attribute const & attr) {
     buffer<name> instances;
     attr.get_instances(p.env(), instances);
 
@@ -511,28 +483,23 @@ static void print_attribute(parser & p, attribute const & attr) {
     unsigned i = instances.size();
     while (i > 0) {
         --i;
-        p.ios().get_regular_stream() << instances[i] << "\n";
+        out << instances[i] << "\n";
     }
 }
 
 environment print_cmd(parser & p) {
-    flycheck_information info(p.ios());
-    environment const & env = p.env();
-    type_checker tc(env);
-    auto out = regular(env, p.ios(), tc);
-    if (info.enabled()) {
-        p.display_information_pos(p.cmd_pos());
-        out << "print result:\n";
-    }
+    auto out = p.mk_message(p.cmd_pos(), INFORMATION);
+    out.set_caption("print result");
+    auto env = p.env();
     if (p.curr() == scanner::token_kind::String) {
         out << p.get_str_val() << endl;
         p.next();
     } else if (p.curr_is_token_or_id(get_raw_tk())) {
         p.next();
         expr e = p.parse_expr();
-        options opts = out.get_options();
+        options opts = out.get_text_stream().get_options();
         opts = opts.update(get_pp_notation_name(), false);
-        out.update_options(opts) << e << endl;
+        out.get_text_stream().update_options(opts) << e << endl;
     } else if (p.curr_is_token_or_id(get_options_tk())) {
         p.next();
         out << p.ios().get_options() << endl;
@@ -541,7 +508,7 @@ environment print_cmd(parser & p) {
         out << "trust level: " << p.env().trust_lvl() << endl;
     } else if (p.curr_is_token_or_id(get_key_equivalences_tk())) {
         p.next();
-        print_key_equivalences(p);
+        print_key_equivalences(p, out);
     } else if (p.curr_is_token_or_id(get_definition_tk())) {
         p.next();
         auto pos = p.pos();
@@ -555,11 +522,11 @@ environment print_cmd(parser & p) {
                 out << "\n";
             declaration const & d = p.env().get(c);
             if (d.is_theorem()) {
-                print_constant(p, "theorem", d);
-                print_definition(p, c, pos);
+                print_constant(p, out, "theorem", d);
+                print_definition(p, out, c, pos);
             } else if (d.is_definition()) {
-                print_constant(p, "definition", d);
-                print_definition(p, c, pos);
+                print_constant(p, out, "definition", d);
+                print_definition(p, out, c, pos);
             } else {
                 throw parser_error(sstream() << "invalid 'print definition', '" << to_user_name(p.env(), c) << "' is not a definition", pos);
             }
@@ -590,26 +557,26 @@ environment print_cmd(parser & p) {
         }
     } else if (p.curr_is_token_or_id(get_prefix_tk())) {
         p.next();
-        print_prefix(p);
+        print_prefix(p, out);
     } else if (p.curr_is_token_or_id(get_aliases_tk())) {
         p.next();
-        print_aliases(p);
+        print_aliases(p, out);
     } else if (p.curr_is_token_or_id(get_axioms_tk())) {
         p.next();
-        return print_axioms(p);
+        print_axioms(p, out);
     } else if (p.curr_is_token_or_id(get_fields_tk())) {
         p.next();
         auto pos = p.pos();
         name S = p.check_constant_next("invalid 'print fields' command, constant expected");
-        print_fields(p, S, pos);
+        print_fields(p, out, S, pos);
     } else if (p.curr_is_token_or_id(get_notation_tk())) {
         p.next();
-        print_notation(p);
+        print_notation(p, out);
     } else if (p.curr_is_token_or_id(get_inductive_tk())) {
         p.next();
         auto pos = p.pos();
         name c = p.check_constant_next("invalid 'print inductive', constant expected");
-        print_inductive(p, c, pos);
+        print_inductive(p, out, c, pos);
     } else if (p.curr_is_token(get_lbracket_tk())) {
         p.next();
         auto pos = p.pos();
@@ -617,23 +584,24 @@ environment print_cmd(parser & p) {
         p.check_token_next(get_rbracket_tk(), "invalid 'print [<attr>]', ']' expected");
 
         if (name == "recursor") {
-            print_recursor_info(p);
+            print_recursor_info(p, out);
         } else if (name == "unify") {
-            print_unification_hints(p);
+            print_unification_hints(p, out);
         } else if (name == "simp") {
-            print_simp_rules(p);
+            print_simp_rules(p, out);
         } else if (name == "congr") {
-            print_congr_rules(p);
+            print_congr_rules(p, out);
         } else {
             if (!is_attribute(p.env(), name))
                 throw parser_error(sstream() << "unknown attribute [" << name << "]", pos);
             auto const & attr = get_attribute(p.env(), name);
-            print_attribute(p, attr);
+            print_attribute(p, out, attr);
         }
-    } else if (print_polymorphic(p)) {
+    } else if (print_polymorphic(p, out)) {
     } else {
         throw parser_error("invalid print command", p.pos());
     }
+    out.report();
     return p.env();
 }
 }
diff --git a/src/frontends/smt2/parser.cpp b/src/frontends/smt2/parser.cpp
index 03042b715c..afce7b244f 100644
--- a/src/frontends/smt2/parser.cpp
+++ b/src/frontends/smt2/parser.cpp
@@ -8,6 +8,7 @@ Author: Daniel Selsam
 #include <stack>
 #include <utility>
 #include <vector>
+#include <library/message_builder.h>
 #include "util/flet.h"
 #include "util/name_map.h"
 #include "util/exception.h"
@@ -27,7 +28,6 @@ Author: Daniel Selsam
 #include "library/io_state.h"
 #include "library/io_state_stream.h"
 #include "library/local_context.h"
-#include "library/error_handling.h"
 #include "library/pp_options.h"
 #include "library/module.h"
 #include "library/trace.h"
@@ -713,9 +713,9 @@ public:
             return ok;
         } catch (throwable const & ex) {
             ok = false;
-            type_context aux_tctx(m_env, m_ios.get_options(), m_lctx);
-            auto out = regular(m_env, m_ios, aux_tctx);
-            ::lean::display_error(out, this, ex);
+            ::lean::message_builder(this, std::make_shared<type_context>(m_env, m_ios.get_options(), m_lctx),
+                                    m_env, m_ios, get_file_name(), get_some_pos(), ERROR)
+                    .set_exception(ex).report();
         }
         return ok;
     }
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 3f2257e6f5..81e52d37bd 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -10,9 +10,10 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   unfold_macros.cpp app_builder.cpp projection.cpp relation_manager.cpp
   export.cpp user_recursors.cpp idx_metavar.cpp noncomputable.cpp
   aux_recursors.cpp norm_num.cpp trace.cpp
-  attribute_manager.cpp error_handling.cpp unification_hint.cpp
+  attribute_manager.cpp unification_hint.cpp
   local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp
   fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp
   mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp
   aux_definition.cpp inverse.cpp library_system.cpp pattern_attribute.cpp choice.cpp
-  locals.cpp normalize.cpp discr_tree.cpp)
+  locals.cpp normalize.cpp discr_tree.cpp
+  messages.cpp message_builder.cpp)
diff --git a/src/library/abstract_parser.h b/src/library/abstract_parser.h
index 7e50ba48cf..de639f5c3e 100644
--- a/src/library/abstract_parser.h
+++ b/src/library/abstract_parser.h
@@ -6,6 +6,7 @@ Author: Sebastian Ullrich
 */
 #pragma once
 #include "kernel/pos_info_provider.h"
+#include <string>
 
 namespace lean {
 /** \brief Exception used to track parsing erros, it does not leak outside of this class. */
@@ -13,6 +14,7 @@ struct parser_error : public exception {
     pos_info m_pos;
     parser_error(char const * msg, pos_info const & p):exception(msg), m_pos(p) {}
     parser_error(sstream const & msg, pos_info const & p):exception(msg), m_pos(p) {}
+    std::string const & get_msg() const { return m_msg; }
     virtual throwable * clone() const { return new parser_error(m_msg.c_str(), m_pos); }
     virtual void rethrow() const { throw *this; }
 };
diff --git a/src/library/error_handling.cpp b/src/library/error_handling.cpp
deleted file mode 100644
index 67be1283e4..0000000000
--- a/src/library/error_handling.cpp
+++ /dev/null
@@ -1,157 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <utility>
-#include <string>
-#include "util/name_set.h"
-#include "kernel/ext_exception.h"
-#include "kernel/for_each_fn.h"
-#include "library/io_state_stream.h"
-#include "library/exception.h"
-#include "library/flycheck.h"
-#include "library/pp_options.h"
-#include "library/error_handling.h"
-
-namespace lean {
-void display_pos(std::ostream & out, options const & o, char const * strm_name, unsigned line, unsigned pos) {
-    out << strm_name << ":";
-    if (o.get_bool("flycheck", false)) {
-        // generate valid line and column for flycheck mode
-        if (line == static_cast<unsigned>(-1))
-            line = 1;
-        if (pos == static_cast<unsigned>(-1))
-            pos = 0;
-    }
-    if (line != static_cast<unsigned>(-1))
-        out << line << ":";
-    if (pos != static_cast<unsigned>(-1))
-        out << pos << ":";
-}
-
-void display_pos(std::ostream & out, char const * strm_name, unsigned line, unsigned pos) {
-    display_pos(out, options(), strm_name, line, pos);
-}
-
-void display_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
-    display_pos(ios.get_stream(), ios.get_options(), strm_name, line, pos);
-}
-
-void display_error_pos(std::ostream & out, options const & o, char const * strm_name, unsigned line, unsigned pos) {
-    display_pos(out, o, strm_name, line, pos);
-    out << " error:";
-}
-
-void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
-    display_error_pos(ios.get_stream(), ios.get_options(), strm_name, line, pos);
-}
-
-void display_warning_pos(std::ostream & out, options const & o, char const * strm_name, unsigned line, unsigned pos) {
-    display_pos(out, o, strm_name, line, pos);
-    out << " warning:";
-}
-
-void display_warning_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
-    display_warning_pos(ios.get_stream(), ios.get_options(), strm_name, line, pos);
-}
-
-void display_warning_pos(io_state_stream const & ios, pos_info_provider const * p, expr const & e) {
-    if (p) {
-        auto pos = p->get_pos_info_or_some(e);
-        display_warning_pos(ios, p->get_file_name(), pos.first, pos.second);
-    } else {
-        ios << "warning:";
-    }
-}
-
-void display_warning_pos(io_state_stream const & ios, pos_info_provider const * p, optional<expr> const & e) {
-    if (e) {
-        display_warning_pos(ios, p, *e);
-    } else {
-        ios << "warning:";
-    }
-}
-
-void display_information_pos(std::ostream & out, options const & o, char const * strm_name, unsigned line, unsigned pos) {
-    display_pos(out, o, strm_name, line, pos);
-    out << " information:";
-}
-
-void display_information_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
-    display_information_pos(ios.get_stream(), ios.get_options(), strm_name, line, pos);
-}
-
-void display_error_pos(std::ostream & out, options const & o, pos_info_provider const * p, expr const & e) {
-    if (p) {
-        auto pos = p->get_pos_info_or_some(e);
-        display_error_pos(out, o, p->get_file_name(), pos.first, pos.second);
-    } else {
-        out << "error:";
-    }
-}
-
-void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, expr const & e) {
-    display_error_pos(ios.get_stream(), ios.get_options(), p, e);
-}
-
-void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, optional<expr> const & e) {
-    if (e) {
-        display_error_pos(ios, p, *e);
-    } else if (p) {
-        auto pos = p->get_some_pos();
-        display_error_pos(ios, p->get_file_name(), pos.first, pos.second);
-    } else {
-        ios << "error:";
-    }
-}
-
-static void display_error_warning_pos(bool is_error, io_state_stream const & ios, pos_info_provider const * p, optional<expr> const & e) {
-    if (is_error)
-        display_error_pos(ios, p, e);
-    else
-        display_warning_pos(ios, p, e);
-}
-
-static void display_error_warning_pos(bool is_error, io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
-    if (is_error)
-        display_error_pos(ios, strm_name, line, pos);
-    else
-        display_warning_pos(ios, strm_name, line, pos);
-}
-
-static void display_error_warning(bool is_error, io_state_stream const & ios, pos_info_provider const * p, throwable const & ex);
-
-static void display_error_warning(bool is_error, io_state_stream const & ios, pos_info_provider const * p, ext_exception const & ex) {
-    display_error_warning_pos(is_error, ios, p, ex.get_main_expr());
-    ios << " " << ex << endl;
-}
-
-static void display_error_warning(bool is_error, io_state_stream const & ios, pos_info_provider const * p, formatted_exception const & ex) {
-    display_error_warning_pos(is_error, ios, p, ex.get_main_expr());
-    ios << " " << ex << endl;
-}
-
-static void display_error_warning(bool is_error, io_state_stream const & ios, pos_info_provider const * p, throwable const & ex) {
-    flycheck_error err(ios.get_stream(), ios.get_options());
-    if (auto k_ex = dynamic_cast<ext_exception const *>(&ex)) {
-        display_error_warning(is_error, ios, p, *k_ex);
-    } else if (auto f_ex = dynamic_cast<formatted_exception const *>(&ex)) {
-        display_error_warning(is_error, ios, p, *f_ex);
-    } else if (p) {
-        display_error_warning_pos(is_error, ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second);
-        ios << " " << ex.what() << endl;
-    } else {
-        ios << (is_error ? "error: " : "warning: ") << ex.what() << endl;
-    }
-}
-
-void display_error(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex) {
-    display_error_warning(true, ios, p, ex);
-}
-
-void display_warning(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex) {
-    display_error_warning(false, ios, p, ex);
-}
-}
diff --git a/src/library/error_handling.h b/src/library/error_handling.h
deleted file mode 100644
index 07b2f0ee78..0000000000
--- a/src/library/error_handling.h
+++ /dev/null
@@ -1,36 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/exception.h"
-#include "kernel/pos_info_provider.h"
-#include "library/io_state_stream.h"
-
-namespace lean {
-void display_pos(std::ostream & out, options const & o, char const * strm_name, unsigned line, unsigned pos);
-void display_pos(std::ostream & out, char const * strm_name, unsigned line, unsigned pos);
-void display_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos);
-/**
-   \brief Display position information associated with \c e (IF avaiable).
-   If it is not available, it just displays "error:"
-*/
-void display_error_pos(std::ostream & out, options const & o, pos_info_provider const * p, expr const & e);
-void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, expr const & e);
-/** \brief Display position information + "error:" */
-void display_error_pos(std::ostream & out, options const & o, char const * strm_name, unsigned line, unsigned pos);
-void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos);
-/** \brief Similar to #display_error_pos, but displays a "warning:" */
-void display_warning_pos(std::ostream & out, options const & o, char const * strm_name, unsigned line, unsigned pos);
-void display_warning_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos);
-void display_information_pos(std::ostream & out, options const & o, char const * strm_name, unsigned line, unsigned pos);
-void display_information_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos);
-/**
-   \brief Display exception in the regular stream of \c ios, using the configuration options and formatter from \c ios.
-   Exceptions that contain expressions use the given \c pos_info_provider (if available) to retrieve line number information.
-*/
-void display_error(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex);
-void display_warning(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex);
-}
diff --git a/src/library/flycheck.cpp b/src/library/flycheck.cpp
index bd1de8019b..050f3f1273 100644
--- a/src/library/flycheck.cpp
+++ b/src/library/flycheck.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/flycheck.h"
-#include "library/error_handling.h"
 
 namespace lean {
 flycheck_scope::flycheck_scope(std::ostream & out, options const & o, char const * kind):
@@ -18,7 +17,7 @@ flycheck_scope::~flycheck_scope() {
 }
 flycheck_output_scope::flycheck_output_scope(io_state const & ios, char const * stream_name, pos_info const & pos) :
         m_stream_name(stream_name), m_pos(pos),
-        m_out(ios.get_regular_stream()),
+        m_ios(ios),
         m_redirected_ios(ios),
         m_scoped_ios(), m_buffer() {
     if (ios.get_options().get_bool("flycheck", false)) {
@@ -34,12 +33,8 @@ flycheck_output_scope::flycheck_output_scope(pos_info_provider const * provider,
 flycheck_output_scope::~flycheck_output_scope() {
     if (enabled()) {
         auto redirected_output = m_buffer->str();
-        if (!redirected_output.empty()) {
-            m_out << "FLYCHECK_BEGIN INFORMATION" << std::endl;
-            display_pos(m_out, m_stream_name, m_pos.first, m_pos.second);
-            m_out << " information:" << std::endl << redirected_output;
-            m_out << "FLYCHECK_END" << std::endl;
-        }
+        if (!redirected_output.empty())
+            m_ios.report(message(m_stream_name, m_pos, INFORMATION, "trace output", redirected_output));
     }
 }
 }
diff --git a/src/library/flycheck.h b/src/library/flycheck.h
index e2e04c9df4..dd0abd7337 100644
--- a/src/library/flycheck.h
+++ b/src/library/flycheck.h
@@ -27,7 +27,7 @@ public:
 class flycheck_output_scope {
     char const *                           m_stream_name;
     pos_info                               m_pos;
-    std::ostream &                         m_out;
+    io_state const &                       m_ios;
     io_state                               m_redirected_ios;
     std::unique_ptr<scope_global_ios>      m_scoped_ios;
     std::shared_ptr<string_output_channel> m_buffer;
@@ -39,19 +39,4 @@ public:
     ~flycheck_output_scope();
     bool enabled() const { return static_cast<bool>(m_scoped_ios); }
 };
-
-struct flycheck_error : public flycheck_scope {
-    flycheck_error(std::ostream & out, options const & o):flycheck_scope(out, o, "ERROR") {}
-    flycheck_error(io_state const & ios):flycheck_scope(ios, "ERROR") {}
-};
-
-struct flycheck_warning : public flycheck_scope {
-    flycheck_warning(std::ostream & out, options const & o):flycheck_scope(out, o, "WARNING") {}
-    flycheck_warning(io_state const & ios):flycheck_scope(ios, "WARNING") {}
-};
-
-struct flycheck_information : public flycheck_scope {
-    flycheck_information(std::ostream & out, options const & o):flycheck_scope(out, o, "INFORMATION") {}
-    flycheck_information(io_state const & ios):flycheck_scope(ios, "INFORMATION") {}
-};
 }
diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp
index 905a683019..6d0440118e 100644
--- a/src/library/io_state.cpp
+++ b/src/library/io_state.cpp
@@ -21,26 +21,30 @@ io_state::io_state():io_state(mk_print_formatter_factory()) {}
 io_state::io_state(formatter_factory const & fmtf):
     m_formatter_factory(fmtf),
     m_regular_channel(std::make_shared<stdout_channel>()),
-    m_diagnostic_channel(std::make_shared<stderr_channel>()) {
+    m_diagnostic_channel(std::make_shared<stderr_channel>()),
+    m_message_channel(std::make_shared<output_channel_message_stream>(m_options, m_regular_channel)) {
 }
 
 io_state::io_state(options const & opts, formatter_factory const & fmtf):
     m_options(opts),
     m_formatter_factory(fmtf),
     m_regular_channel(std::make_shared<stdout_channel>()),
-    m_diagnostic_channel(std::make_shared<stderr_channel>()) {
+    m_diagnostic_channel(std::make_shared<stderr_channel>()),
+    m_message_channel(std::make_shared<output_channel_message_stream>(m_options, m_regular_channel)) {
 }
 io_state::io_state(io_state const & ios, std::shared_ptr<output_channel> const & r, std::shared_ptr<output_channel> const & d):
     m_options(ios.m_options),
     m_formatter_factory(ios.m_formatter_factory),
     m_regular_channel(r),
-    m_diagnostic_channel(d) {
+    m_diagnostic_channel(d),
+    m_message_channel(ios.m_message_channel) {
 }
 io_state::io_state(io_state const & ios, options const & o):
     m_options(o),
     m_formatter_factory(ios.m_formatter_factory),
     m_regular_channel(ios.m_regular_channel),
-    m_diagnostic_channel(ios.m_diagnostic_channel) {
+    m_diagnostic_channel(ios.m_diagnostic_channel),
+    m_message_channel(ios.m_message_channel) {
 }
 
 io_state::~io_state() {}
diff --git a/src/library/io_state.h b/src/library/io_state.h
index 3b64f42395..e937507d3c 100644
--- a/src/library/io_state.h
+++ b/src/library/io_state.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "util/output_channel.h"
+#include "library/messages.h"
 #include "util/sexpr/options.h"
 #include "kernel/expr.h"
 
@@ -22,6 +23,7 @@ class io_state {
     formatter_factory               m_formatter_factory;
     std::shared_ptr<output_channel> m_regular_channel;
     std::shared_ptr<output_channel> m_diagnostic_channel;
+    std::shared_ptr<message_stream> m_message_channel;
 public:
     io_state();
     io_state(formatter_factory const & fmtf);
@@ -32,13 +34,18 @@ public:
 
     options const & get_options() const { return m_options; }
     formatter_factory const & get_formatter_factory() const { return m_formatter_factory; }
+    std::shared_ptr<message_stream> const & get_message_channel_ptr() const { return m_message_channel; }
     std::shared_ptr<output_channel> const & get_regular_channel_ptr() const { return m_regular_channel; }
     std::shared_ptr<output_channel> const & get_diagnostic_channel_ptr() const { return m_diagnostic_channel; }
+    message_stream & get_message_channel() const { return *m_message_channel; }
     output_channel & get_regular_channel() const { return *m_regular_channel; }
     output_channel & get_diagnostic_channel() const { return *m_diagnostic_channel; }
     std::ostream & get_regular_stream() const { return m_regular_channel->get_stream(); }
     std::ostream & get_diagnostic_stream() const { return m_diagnostic_channel->get_stream(); }
 
+    void report(message const & msg) const { if (m_message_channel) m_message_channel->report(msg); }
+
+    void set_message_channel(std::shared_ptr<message_stream> const & out) { m_message_channel = out; }
     void set_regular_channel(std::shared_ptr<output_channel> const & out);
     void set_diagnostic_channel(std::shared_ptr<output_channel> const & out);
     void set_options(options const & opts);
@@ -47,6 +54,7 @@ public:
         set_options(get_options().update(n, v));
     }
 };
+
 /** \brief Return a dummy io_state that is meant to be used in contexts that require an io_state, but it is not really used */
 io_state const & get_dummy_ios();
 
diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h
index a24a83fe1f..6ee90857d7 100644
--- a/src/library/io_state_stream.h
+++ b/src/library/io_state_stream.h
@@ -19,13 +19,16 @@ protected:
     environment                     m_env;
     formatter                       m_formatter;
     std::shared_ptr<output_channel> m_stream;
+public:
     io_state_stream(environment const & env, formatter const & fmt, std::shared_ptr<output_channel> const & s):
         m_env(env), m_formatter(fmt), m_stream(s) {}
-public:
-    io_state_stream(environment const & env, io_state const & ios, abstract_type_context & ctx, bool regular = true):
+    io_state_stream(environment const & env, io_state const & ios, abstract_type_context & ctx, std::shared_ptr<output_channel> const & stream):
         m_env(env), m_formatter(ios.get_formatter_factory()(env, ios.get_options(), ctx)),
-        m_stream(regular ? ios.get_regular_channel_ptr() : ios.get_diagnostic_channel_ptr()) {}
+        m_stream(stream) {}
+    io_state_stream(environment const & env, io_state const & ios, abstract_type_context & ctx, bool regular = true):
+        io_state_stream(env, ios, ctx, regular ? ios.get_regular_channel_ptr() : ios.get_diagnostic_channel_ptr()) {}
     std::ostream & get_stream() const { return m_stream->get_stream(); }
+    std::shared_ptr<output_channel> get_channel() const { return m_stream; }
     void flush() { get_stream().flush(); }
     formatter const & get_formatter() const { return m_formatter; }
     options get_options() const { return m_formatter.get_options(); }
diff --git a/src/library/message_builder.cpp b/src/library/message_builder.cpp
new file mode 100644
index 0000000000..97fb4a7fb1
--- /dev/null
+++ b/src/library/message_builder.cpp
@@ -0,0 +1,55 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Gabriel Ebner
+*/
+#include "library/message_builder.h"
+#include "library/type_context.h"
+#include <string>
+
+namespace lean {
+
+message_builder::message_builder(pos_info_provider const * provider,
+                                 std::shared_ptr<abstract_type_context> const & tc,
+                                 environment const & env, io_state const & ios,
+                                 std::string const & file_name, const pos_info & pos,
+                                 message_severity severity) :
+    m_pos_info_provider(provider), m_ios(ios), m_tc(tc),
+    m_file_name(file_name), m_pos(pos), m_severity(severity),
+    m_caption(), m_text(std::make_shared<string_output_channel>()),
+    m_text_stream(env, ios.get_formatter_factory()(env, ios.get_options(), *tc), m_text) {}
+
+message_builder::message_builder(environment const & env, io_state const & ios,
+                                 std::string const & file_name, pos_info const & pos,
+                                 message_severity severity) :
+        message_builder(nullptr, std::make_shared<type_context>(env, ios.get_options()),
+                        env, ios, file_name, pos, severity) {}
+
+message message_builder::build() {
+    auto text = m_text->str();
+    if (!text.empty() && *text.rbegin() == '\n')
+        text = text.substr(0, text.size() - 1);
+    return message(m_file_name, m_pos, m_severity, m_caption, text);
+}
+
+message_builder & message_builder::set_exception(throwable const & ex) {
+    if (auto ext_ex = dynamic_cast<ext_exception const *>(&ex)) {
+        if (m_pos_info_provider && ext_ex->get_main_expr()) {
+            if (auto main_pos = m_pos_info_provider->get_pos_info(*ext_ex->get_main_expr()))
+                m_pos = *main_pos;
+        }
+        *this << *ext_ex;
+    } else if (auto f_ex = dynamic_cast<formatted_exception const *>(&ex)) {
+        if (m_pos_info_provider && f_ex->get_main_expr()) {
+            if (auto main_pos = m_pos_info_provider->get_pos_info(*f_ex->get_main_expr()))
+                m_pos = *main_pos;
+        }
+        *this << f_ex->pp();
+    } else {
+        *this << ex.what();
+    }
+    return *this;
+}
+
+}
diff --git a/src/library/message_builder.h b/src/library/message_builder.h
new file mode 100644
index 0000000000..9b025e428a
--- /dev/null
+++ b/src/library/message_builder.h
@@ -0,0 +1,55 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Gabriel Ebner
+*/
+#pragma once
+#include <string>
+#include "kernel/pos_info_provider.h"
+#include "util/output_channel.h"
+#include "util/exception.h"
+#include "library/io_state_stream.h"
+
+namespace lean {
+
+/** Buider for a message object.  Automatically reports the message on destruction. */
+class message_builder {
+    pos_info_provider const *              m_pos_info_provider;
+    io_state const &                       m_ios;
+    std::shared_ptr<abstract_type_context> m_tc;
+    std::string                            m_file_name;
+    pos_info                               m_pos;
+    message_severity                       m_severity;
+    std::string                            m_caption;
+    std::shared_ptr<string_output_channel> m_text;
+    io_state_stream                        m_text_stream;
+
+public:
+    message_builder(pos_info_provider const * provider,
+                    std::shared_ptr<abstract_type_context> const & tc,
+                    environment const & env, io_state const & ios,
+                    std::string const & file_name, pos_info const & pos,
+                    message_severity severity);
+    message_builder(environment const & env, io_state const & ios,
+                    std::string const & file_name, pos_info const & pos,
+                    message_severity severity);
+
+    message build();
+    void report() { m_ios.report(build()); }
+
+    message_builder & set_file_name(std::string const & file_name) { m_file_name = file_name; return *this; }
+    message_builder & set_pos(pos_info const & pos) { m_pos = pos; return *this; }
+    message_builder & set_severity(message_severity severity) { m_severity = severity; return *this; }
+    message_builder & set_caption(std::string const & caption) { m_caption = caption; return *this; }
+
+    formatter const & get_formatter() const { return m_text_stream.get_formatter(); }
+
+    io_state_stream & get_text_stream() { return m_text_stream; }
+    template <typename T>
+    message_builder & operator<<(T const & t) { m_text_stream << t; return *this; }
+
+    message_builder & set_exception(throwable const & ex);
+};
+
+}
diff --git a/src/library/messages.cpp b/src/library/messages.cpp
new file mode 100644
index 0000000000..a49934d531
--- /dev/null
+++ b/src/library/messages.cpp
@@ -0,0 +1,41 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Gabriel Ebner
+*/
+#include "library/messages.h"
+#include "library/flycheck.h"
+
+namespace lean {
+
+message::message(parser_exception const & ex) :
+        message(ex.get_file_name(), pos_info(ex.get_line(), ex.get_pos()),
+                ERROR, ex.get_msg()) {}
+
+static char const * flycheck_kind_of_severity(message_severity severity) {
+    switch (severity) {
+        case INFORMATION: return "INFORMATION";
+        case WARNING:     return "WARNING";
+        case ERROR:       return "ERROR";
+        default: lean_unreachable();
+    }
+}
+
+void output_channel_message_stream::report(message const & msg) {
+    flycheck_scope flycheck(m_out->get_stream(), m_options, flycheck_kind_of_severity(msg.get_severity()));
+    if (flycheck.enabled() || msg.get_severity() != INFORMATION) {
+        m_out->get_stream() << msg.get_file_name()
+                            << ":" << msg.get_pos().first << ":" << msg.get_pos().second << ": ";
+        switch (msg.get_severity()) {
+            case INFORMATION: break;
+            case WARNING: m_out->get_stream() << "warning: "; break;
+            case ERROR:   m_out->get_stream() << "error: ";   break;
+        }
+        if (!msg.get_caption().empty())
+            m_out->get_stream() << msg.get_caption() << ":\n";
+    }
+    m_out->get_stream() << msg.get_text() << "\n";
+}
+
+}
diff --git a/src/library/messages.h b/src/library/messages.h
new file mode 100644
index 0000000000..cbfc0662e2
--- /dev/null
+++ b/src/library/messages.h
@@ -0,0 +1,58 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Gabriel Ebner
+*/
+#pragma once
+#include <string>
+#include "kernel/pos_info_provider.h"
+#include "util/output_channel.h"
+#include "util/exception.h"
+
+namespace lean {
+
+enum message_severity { INFORMATION, WARNING, ERROR };
+
+class message {
+    std::string      m_file_name;
+    pos_info         m_pos;
+    message_severity m_severity;
+    std::string      m_caption, m_text;
+public:
+    message(std::string const & file_name, pos_info const & pos,
+            message_severity severity, std::string const & caption, std::string const & text) :
+            m_file_name(file_name), m_pos(pos),
+            m_severity(severity), m_caption(caption), m_text(text) {}
+    message(std::string const & file_name, pos_info const & pos,
+            message_severity severity, std::string const & text) :
+            message(file_name, pos, severity, std::string(), text) {}
+    message(std::string const & file_name, pos_info const & pos,
+            message_severity severity) :
+            message(file_name, pos, severity, std::string()) {}
+    message(parser_exception const & ex);
+
+    std::string get_file_name() const { return m_file_name; }
+    pos_info get_pos() const { return m_pos; }
+    message_severity get_severity() const { return m_severity; }
+    std::string get_caption() const { return m_caption; }
+    std::string get_text() const { return m_text; }
+};
+
+class message_stream {
+public:
+    virtual ~message_stream() {}
+    virtual void report(message const & msg) = 0;
+};
+
+class output_channel_message_stream : public message_stream {
+    options                         m_options;
+    std::shared_ptr<output_channel> m_out;
+public:
+    output_channel_message_stream(options const & opts, std::shared_ptr<output_channel> const & out) :
+            m_options(opts), m_out(out) {}
+    ~output_channel_message_stream() {}
+    void report(message const & msg) override;
+};
+
+}
diff --git a/src/shell/emscripten.cpp b/src/shell/emscripten.cpp
index 9bb03b622c..701d863a1c 100644
--- a/src/shell/emscripten.cpp
+++ b/src/shell/emscripten.cpp
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/standard_kernel.h"
 #include "library/type_context.h"
-#include "library/error_handling.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/parser.h"
 #include "init/init.h"
@@ -36,10 +35,7 @@ public:
             bool keep_proofs = false;
             env = import_modules(env, base, 1, &mod, num_threads, keep_proofs, ios);
         } catch (lean::exception & ex) {
-            simple_pos_info_provider pp("import_module");
-            type_context tc(env, ios.get_options());
-            auto out = diagnostic(env, ios, tc);
-            lean::display_error(out, &pp, ex);
+            lean::message_builder(env, ios, "import_module", lean::pos_info(1, 1), lean::ERROR).set_exception(ex).report();
             return 1;
         }
         return 0;
@@ -54,11 +50,8 @@ public:
                 ok = false;
             }
         } catch (lean::exception & ex) {
-            simple_pos_info_provider pp(input_filename.c_str());
+            lean::message_builder(env, ios, input_filename, lean::pos_info(1, 1), lean::ERROR).set_exception(ex).report();
             ok = false;
-            type_context tc(env, ios.get_options());
-            auto out = diagnostic(env, ios, tc);
-            lean::display_error(out, &pp, ex);
         }
         return ok ? 0 : 1;
     }
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 02d1ea9866..4b68fe30c2 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -32,7 +32,7 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 #include "library/definition_cache.h"
 #include "library/export.h"
-#include "library/error_handling.h"
+#include "library/message_builder.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/dependencies.h"
@@ -360,9 +360,10 @@ int main(int argc, char ** argv) {
             } catch (lean::exception & ex) {
                 ok = false;
                 type_context tc(env, ios.get_options());
-                auto out = diagnostic(env, ios, tc);
                 simple_pos_info_provider pp(argv[i]);
-                lean::display_error(out, &pp, ex);
+                lean::message_builder(&pp, std::make_shared<type_context>(env, ios.get_options()),
+                                      env, ios, argv[i], pos_info(1, 1), lean::ERROR)
+                        .set_exception(ex).report();
             }
         }
         return ok ? 0 : 1;
@@ -381,16 +382,11 @@ int main(int argc, char ** argv) {
                 cache.load(in);
         } catch (lean::throwable & ex) {
             cache_ptr = nullptr;
-            // I'm using flycheck_error instead off flycheck_warning because
-            // the :error-patterns at lean-flycheck.el do not work after
-            // I add a rule for FLYCHECK_WARNING.
-            // Same for display_error_pos vs display_warning_pos.
-            lean::flycheck_error warn(ios);
-            if (optind < argc)
-                display_error_pos(ios.get_regular_stream(), ios.get_options(), argv[optind], 1, 0);
-            ios.get_regular_stream()
-                << "failed to load cache file '" << cache_name << "', "
-                << ex.what() << ". cache is going to be ignored\n";
+            auto out = lean::message_builder(env, ios, argv[optind], lean::pos_info(1, 1), lean::WARNING);
+            out << "failed to load cache file '" << cache_name << "'\n";
+            out.set_exception(ex);
+            out << "cache is going to be ignored";
+            out.report();
         }
     }
     try {
@@ -405,11 +401,8 @@ int main(int argc, char ** argv) {
                     ok = false;
                 }
             } catch (lean::exception & ex) {
-                simple_pos_info_provider pp(argv[i]);
                 ok = false;
-                type_context tc(env, ios.get_options());
-                auto out = diagnostic(env, ios, tc);
-                lean::display_error(out, &pp, ex);
+                lean::message_builder(env, ios, argv[i], lean::pos_info(1, 1), lean::ERROR).set_exception(ex).report();
             }
         }
         if (save_cache) {
@@ -434,9 +427,7 @@ int main(int argc, char ** argv) {
         }
         return ok ? 0 : 1;
     } catch (lean::throwable & ex) {
-        type_context tc(env, ios.get_options());
-        auto out = diagnostic(env, ios, tc);
-        lean::display_error(out, nullptr, ex);
+        lean::message_builder(env, ios, "<unknown>", lean::pos_info(1, 1), lean::ERROR).set_exception(ex).report();
     } catch (std::bad_alloc & ex) {
         std::cerr << "out of memory" << std::endl;
         return 1;
diff --git a/src/util/exception.h b/src/util/exception.h
index 8225e3a5e3..98d768e4ed 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -54,6 +54,7 @@ public:
     unsigned get_line() const { return m_line; }
     unsigned get_pos() const { return m_pos; }
     std::string const & get_file_name() const { return m_fname; }
+    std::string const & get_msg() const { return m_msg; }
     virtual throwable * clone() const { return new parser_exception(m_msg, m_fname.c_str(), m_line, m_pos); }
     virtual void rethrow() const { throw *this; }
     parser_exception update_line(unsigned line_delta) const { return parser_exception(m_msg, m_fname.c_str(), m_line + line_delta, m_pos); }
diff --git a/tests/lean/char_lits.lean.expected.out b/tests/lean/char_lits.lean.expected.out
index 7785d9c84f..ad0caa1dd9 100644
--- a/tests/lean/char_lits.lean.expected.out
+++ b/tests/lean/char_lits.lean.expected.out
@@ -4,4 +4,7 @@
 '\\'
 aaa\
 
-aaa'
\ No newline at end of file
+
+
+
+aaa'
diff --git a/tests/lean/concrete_instance.lean.expected.out b/tests/lean/concrete_instance.lean.expected.out
index 8154e4e3cd..d96e46aae7 100644
--- a/tests/lean/concrete_instance.lean.expected.out
+++ b/tests/lean/concrete_instance.lean.expected.out
@@ -1,8 +1,8 @@
 @mul.{1} nat nat.has_mul a b : nat
 @add.{1} nat nat.has_add a b : nat
-concrete_instance.lean:8:9:failed to generate bytecode for 'nat.semigroup'
-concrete_instance.lean:8:0: warning: code generation failed, VM does not have code for 'sorry'
-concrete_instance.lean:9:9:failed to generate bytecode for 'nat.add_semigroup'
-concrete_instance.lean:9:0: warning: code generation failed, VM does not have code for 'sorry'
+concrete_instance.lean:8:9: warning: failed to generate bytecode for 'nat.semigroup'
+code generation failed, VM does not have code for 'sorry'
+concrete_instance.lean:9:9: warning: failed to generate bytecode for 'nat.add_semigroup'
+code generation failed, VM does not have code for 'sorry'
 @mul.{1} nat nat.has_mul a b : nat
 @add.{1} nat nat.has_add a b : nat
diff --git a/tests/lean/elab_error_msgs.lean.expected.out b/tests/lean/elab_error_msgs.lean.expected.out
index e124407afb..37f32d7d78 100644
--- a/tests/lean/elab_error_msgs.lean.expected.out
+++ b/tests/lean/elab_error_msgs.lean.expected.out
@@ -18,7 +18,6 @@ but is expected to have type
   ?m_2 ?m_3 ?m_3
 Additional information:
 elab_error_msgs.lean:9:0: context: 'eliminator' elaboration is not used for 'bogus_elim' because a (reliable) way to synthesize 'a', which occurs in the resulting type, was not found
-
 elab_error_msgs.lean:13:20: error: failed to synthesize type class instance for
 a b : Prop,
 h : a ∧ b ∧ b,
diff --git a/tests/lean/unification_hints1.lean.expected.out b/tests/lean/unification_hints1.lean.expected.out
index 66ed5ea9ef..33bb601915 100644
--- a/tests/lean/unification_hints1.lean.expected.out
+++ b/tests/lean/unification_hints1.lean.expected.out
@@ -1,23 +1,23 @@
 g x y =?= f z
-fail
+unification failed
 g x y =?= f z
 g x y =?= f z
-success
+unification successful
 unification hints:
 (toy.g, toy.f) g #1 #0 =?= f z {}
 n + 1 =?= succ n
-fail
+unification failed
 n + 1 =?= succ n
 n + 1 =?= succ n
-success
+unification successful
 unification hints:
 (add, nat.succ) #4 + 1 =?= succ #3 {#4 =?= #3}
 (toy.g, toy.f) toy.g #1 #0 =?= toy.f toy.z {}
 Canonical.carrier A_canonical =?= A
-fail
+unification failed
 Canonical.carrier A_canonical =?= A
 Canonical.carrier A_canonical =?= A
-success
+unification successful
 unification hints:
 (add, nat.succ) #4 + 1 =?= succ #3 {#4 =?= #3}
 (toy.g, toy.f) toy.g #1 #0 =?= toy.f toy.z {}