feat: default pp if pp expr/syntax/level without context

src/Lean/Message.lean

@@ -141,14 +141,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)