From 87131f455ff1af07920343c896bdbab34bd8a4b7 Mon Sep 17 00:00:00 2001
From: L Lllvvuu <git@llllvvuu.dev>
Date: Wed, 12 Jun 2024 00:18:13 -0700
Subject: [PATCH] feat: default pp if pp expr/syntax/level without context

---
 src/Lean/Message.lean | 33 ++++++++++++++++++++++++++++-----
 1 file changed, 28 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 033e9cea05d74..ca9496c1adfdc 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -107,7 +107,8 @@ def lazy (f : PPContext → IO MessageData)
     (hasSyntheticSorry : MetavarContext → Bool := fun _ => false) : MessageData :=
   .ofLazy (hasSyntheticSorry := hasSyntheticSorry) fun ctx? => do
     let msg ← match ctx? with
-      | .none => pure (.ofFormat "(invalid MessageData.lazy, missing context)")
+      | .none =>
+        pure (.ofFormat "(invalid MessageData.lazy, missing context)") -- see `addMessageContext`
       | .some ctx => f ctx
     return Dynamic.mk msg
 
@@ -141,14 +142,31 @@ def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext :=
 def ofSyntax (stx : Syntax) : MessageData :=
   -- discard leading/trailing whitespace
   let stx := stx.copyHeadTailInfoFrom .missing
-  .lazy fun ctx => ofFormat <$> ppTerm ctx ⟨stx⟩ -- HACK: might not be a term
+  .ofLazy
+    (fun ctx? => do
+      let msg ← ofFormat <$> match ctx? with
+        | .none => pure stx.formatStx
+        | .some ctx => ppTerm ctx ⟨stx⟩ -- HACK: might not be a term
+      return Dynamic.mk msg)
+    (fun _ => false)
 
 def ofExpr (e : Expr) : MessageData :=
-  .lazy (fun ctx => ofFormatWithInfos <$> ppExprWithInfos ctx e)
-        (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry)
+  .ofLazy
+    (fun ctx? => do
+      let msg ← ofFormatWithInfos <$> match ctx? with
+        | .none => pure (format (toString e))
+        | .some ctx => ppExprWithInfos ctx e
+      return Dynamic.mk msg)
+    (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry)
 
 def ofLevel (l : Level) : MessageData :=
-  .lazy fun ctx => ofFormat <$> ppLevel ctx l
+  .ofLazy
+    (fun ctx? => do
+      let msg ← ofFormat <$> match ctx? with
+        | .none => pure (format l)
+        | .some ctx => ppLevel ctx l
+      return Dynamic.mk msg)
+    (fun _ => false)
 
 def ofName (n : Name) : MessageData := ofFormat (format n)
 
@@ -385,6 +403,11 @@ def indentExpr (e : Expr) : MessageData :=
   indentD e
 
 class AddMessageContext (m : Type → Type) where
+  /-- Without context, a `MessageData` object may be be missing information
+      needed to pretty print with hover info, or may print an error. Hence,
+      `addMessageContext` should be called on all constructed `MessageData`
+      (e.g. via `m!`) before taking it out of context (e.g. leaving `MetaM` or
+      `CoreM`). -/
   addMessageContext : MessageData → m MessageData
 
 export AddMessageContext (addMessageContext)