From 310fc986c10efeda6ad270c112ed2dfe5e26adc7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 17 Sep 2020 15:08:36 +0200
Subject: [PATCH] chore: MetaHasEval TermElabM: print messages

---
 src/Lean/Elab/Term.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 496a059823..b7ff689090 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1268,7 +1268,12 @@ Prod.fst <$> x.run ctx s
 pure (a, sCore, sMeta, s)
 
 instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (TermElabM α) :=
-⟨fun env opts x _ => MetaHasEval.eval env opts $ x.run' mkSomeContext⟩
+⟨fun env opts x _ =>
+  let x := finally x do {
+    s ← get;
+    liftIO $ s.messages.forM fun msg => msg.toString >>= IO.println
+  };
+  MetaHasEval.eval env opts $ x.run' mkSomeContext⟩
 
 end Term