From 06cf5bf3fe5e1e8e17f980f84ac154c8a01e7134 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Nov 2019 08:39:07 -0800 Subject: [PATCH] chore: use dummy pretty printer for now --- library/Init/Lean/Message.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/Init/Lean/Message.lean b/library/Init/Lean/Message.lean index de66eea113..14a181a434 100644 --- a/library/Init/Lean/Message.lean +++ b/library/Init/Lean/Message.lean @@ -48,8 +48,8 @@ partial def formatAux : Option (Environment × MetavarContext × LocalContext) | _, ofSyntax s => s.formatStx | _, ofLevel u => fmt u | _, ofName n => fmt n -| none, ofExpr e => "" -| some (env, mctx, lctx), ofExpr e => "" -- TODO: invoke pretty printer +| none, ofExpr e => format (toString e) +| some (env, mctx, lctx), ofExpr e => format (toString e) -- TODO: invoke pretty printer | _, context env mctx lctx d => formatAux (some (env, mctx, lctx)) d | ctx, tagged cls d => Format.sbracket (format cls) ++ " " ++ formatAux ctx d | ctx, nest n d => Format.nest n (formatAux ctx d)