From 16099189f2c24b74590d5339c14703fb01cf335b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Oct 2019 14:57:26 -0700
Subject: [PATCH] chore: minor adjustments

---
 library/Init/Lean/Message.lean |  6 +++---
 tests/lean/run/trace.lean      | 10 +++++-----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/library/Init/Lean/Message.lean b/library/Init/Lean/Message.lean
index e7f0406497..421abd5cd7 100644
--- a/library/Init/Lean/Message.lean
+++ b/library/Init/Lean/Message.lean
@@ -49,17 +49,17 @@ partial def formatAux : Option (Environment × MetavarContext × LocalContext) 
 | none, ofExpr e                   => "<expr>"
 | some (env, mctx, lctx), ofExpr e => "<expr>" -- TODO: invoke pretty printer
 | _, context env mctx lctx d       => formatAux (some (env, mctx, lctx)) d
-| ctx, tagged cls d                => Format.sbracket (format cls) ++ " " ++ Format.nest 2 (formatAux ctx d)
+| ctx, tagged cls d                => Format.sbracket (format cls) ++ " " ++ formatAux ctx d
 | ctx, nest n d                    => Format.nest n (formatAux ctx d)
 | ctx, compose d₁ d₂               => formatAux ctx d₁ ++ formatAux ctx d₂
 | ctx, group d                     => Format.group (formatAux ctx d)
-| ctx, node ds                     => ds.foldl (fun r d => r ++ Format.line ++ formatAux ctx d) Format.nil
+| ctx, node ds                     => Format.nest 2 $ ds.foldl (fun r d => r ++ Format.line ++ formatAux ctx d) Format.nil
 
 instance : HasAppend MessageData := ⟨compose⟩
 
 instance : HasFormat MessageData := ⟨fun d => formatAux none d⟩
 
-instance : HasCoe String MessageData := ⟨fun s => ofFormat s⟩
+instance coeOfFormat : HasCoe Format MessageData := ⟨ofFormat⟩
 
 end MessageData
 
diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean
index e7c0f5e617..173a644885 100644
--- a/tests/lean/run/trace.lean
+++ b/tests/lean/run/trace.lean
@@ -7,15 +7,15 @@ structure MyState :=
 
 abbrev M := ReaderT Options (EState String MyState)
 
+/- We can enable tracing for a monad M by adding an instance of `SimpleMonadTracerAdapter M` -/
 instance : SimpleMonadTracerAdapter M :=
 { getOptions       := read,
-  getTraceState    := do { s ← get; pure s.traceState },
-  modifyTraceState := fun f =>
-    modify $ fun s => { traceState := f s.traceState, .. s } }
+  getTraceState    := MyState.traceState <$> get,
+  modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } }
 
 def tst1 : M Unit :=
-do trace `module (fun _ => ("hello" : MessageData));
-   trace `module (fun _ => ("world" : MessageData));
+do trace `module (fun _ => ("hello" ++ MessageData.nest 9 (Format.line ++ "world" : MessageData)));
+   trace `module (fun _ => ("another message" : MessageData));
    pure ()
 
 def tst2 (b : Bool) : M Unit :=