From a99523b4b3a970da88ad5215129232d4536df299 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 Jan 2020 13:20:54 -0800
Subject: [PATCH] feat: add `set_option ppOld false` option for disabling
 `ppOld`

The old pretty printer often sucks.
---
 src/Init/Lean/Util/Message.lean | 11 ++++++++++-
 tests/lean/run/meta2.lean       | 12 ++++++++++++
 2 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Util/Message.lean b/src/Init/Lean/Util/Message.lean
index 379eab12b0..1917eca524 100644
--- a/src/Init/Lean/Util/Message.lean
+++ b/src/Init/Lean/Util/Message.lean
@@ -63,7 +63,12 @@ partial def formatAux : Option MessageDataContext → MessageData → Format
 | some ctx,  ofSyntax s        => s.formatStx (getSyntaxMaxDepth ctx.opts)
 | none,      ofSyntax s        => s.formatStx
 | none,      ofExpr e          => format (toString e)
-| some ctx,  ofExpr e          => ppOld ctx.env ctx.mctx ctx.lctx ctx.opts (ctx.mctx.instantiateMVars e).1 -- TODO: replace with new pretty printer
+| some ctx,  ofExpr e          =>
+  let e := (ctx.mctx.instantiateMVars e).1;
+  if ctx.opts.getBool `ppOld true then
+    ppOld ctx.env ctx.mctx ctx.lctx ctx.opts e -- TODO: replace with new pretty printer
+  else
+    format (toString e)
 | _,         withContext ctx d => formatAux (some ctx) d
 | ctx,       tagged cls d      => Format.sbracket (format cls) ++ " " ++ formatAux ctx d
 | ctx,       nest n d          => Format.nest n (formatAux ctx d)
@@ -171,5 +176,9 @@ log.msgs.forM f
 def toList (log : MessageLog) : List Message :=
 (log.msgs.foldl (fun acc msg => msg :: acc) []).reverse
 
+-- TODO: remove after we remove ppOld
+@[init] def ppOldOption : IO Unit :=
+registerOption `ppOld { defValue := true, group := "", descr := "disable/enable old pretty printer" }
+
 end MessageLog
 end Lean
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 8d0d28f0be..8c9a5c0b59 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -409,3 +409,15 @@ do print "----- tst25 -----";
    pure ()
 
 #eval tst25
+
+def tst26 : MetaM Unit := do
+print "----- tst26 -----";
+m1 ← mkFreshExprMVar (mkArrow nat nat);
+m2 ← mkFreshExprMVar nat;
+m3 ← mkFreshExprMVar nat;
+check $ isDefEq (mkApp m1 m2) m3;
+pure ()
+
+set_option ppOld false
+
+#eval tst26