From 5349a73655501604bfbbc826746031bda6be9cce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 27 Aug 2020 11:22:47 -0700 Subject: [PATCH] chore: add `MessageData.nestD` "default nest" --- src/Lean/Message.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 6044d109bc..77919f77d9 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -180,8 +180,11 @@ def toList (log : MessageLog) : List Message := end MessageLog +def MessageData.nestD (msg : MessageData) : MessageData := +MessageData.nest 2 msg + def indentExpr (msg : MessageData) : MessageData := -MessageData.nest 2 (Format.line ++ msg) +MessageData.nestD (Format.line ++ msg) namespace KernelException