fix: make sure #check id heeds pp.raw (leanprover#6181)

This PR fixes a bug where the signature pretty printer would ignore the
current setting of `pp.raw`. This fixes an issue where `#check ident`
would not heed `pp.raw`. Closes leanprover#6090.

src/Lean/PrettyPrinter.lean

@@ -91,9 +91,12 @@ open Delaborator in
 /-- Pretty-prints a declaration `c` as `c.{<levels>} <params> : <type>`. -/
 def ppSignature (c : Name) : MetaM FormatWithInfos := do
   let decl ← getConstInfo c
-  let e := .const c (decl.levelParams.map mkLevelParam)
-  let (stx, infos) ← delabCore e (delab := delabConstWithSignature)
-  return ⟨← ppTerm ⟨stx⟩, infos⟩  -- HACK: not a term
+  let e := Expr.const c (decl.levelParams.map mkLevelParam)
+  if pp.raw.get (← getOptions) then
+    return s!"{e} : {decl.type}"
+  else
+    let (stx, infos) ← delabCore e (delab := delabConstWithSignature)
+    return ⟨← ppTerm ⟨stx⟩, infos⟩  -- HACK: not a term
 
 private partial def noContext : MessageData → MessageData
   | MessageData.withContext _   msg => noContext msg

tests/lean/root.lean.expected.out

@@ -7,7 +7,7 @@ root.lean:35:14-35:22: error: protected declarations must be in a namespace
 root.lean:41:7-41:8: error: unknown identifier 'h'
 root.lean:43:7-43:8: error: unknown identifier 'f'
 Bla.f (x : Nat) : Nat
-prv (x : Nat) : Nat
+_private.root.0.prv : Nat -> Nat
 root.lean:90:89-90:93: error: unsolved goals
 x : Nat
 ⊢ isEven (x + 1 + 1) = isEven x

tests/lean/run/6090.lean

@@ -0,0 +1,30 @@
+/-!
+# Make sure `#check` heeds `pp.raw`
+https://github.com/leanprover/lean4/issues/6090
+-/
+
+section
+/-- info: id.{u} {α : Sort u} (a : α) : α -/
+#guard_msgs in #check id
+/-- info: @id : {α : Sort u_1} → α → α -/
+#guard_msgs in #check @id
+-- '#print' was unaffected, but throw in a test anyway.
+/--
+info: def id.{u} : {α : Sort u} → α → α :=
+fun {α} a => a
+-/
+#guard_msgs in #print id
+
+set_option pp.raw true
+
+/-- info: id.{u} : forall {α : Sort.{u}}, α -> α -/
+#guard_msgs in #check id
+/-- info: id.{u_1} : forall {α : Sort.{u_1}}, α -> α -/
+#guard_msgs in #check @id
+-- '#print' was unaffected, but throw in a test anyway.
+/--
+info: def id.{u} : forall {α : Sort.{u}}, α -> α :=
+fun {α : Sort.{u}} (a : α) => a
+-/
+#guard_msgs in #print id
+end