feat: add set_option ppOld false option for disabling ppOld

The old pretty printer often sucks.

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

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