fix: quoting single quote Char (''') (#8742)

This PR fixes a bug where the single-quote character `Char.ofNat 39`
would delaborate as `'''`, which causes a parse error if pasted back in
to the source code.

---------

Co-authored-by: Kyle Miller <[email protected]>

Author: plp127

src/Init/Data/Repr.lean

@@ -342,11 +342,12 @@ instance : Repr Int where
 def hexDigitRepr (n : Nat) : String :=
   String.singleton <| Nat.digitChar n
 
-def Char.quoteCore (c : Char) : String :=
+def Char.quoteCore (c : Char) (inString : Bool := false) : String :=
   if       c = '\n' then "\\n"
   else if  c = '\t' then "\\t"
   else if  c = '\\' then "\\\\"
   else if  c = '\"' then "\\\""
+  else if !inString && c = '\'' then "\\\'"
   else if  c.toNat <= 31 ∨ c = '\x7f' then "\\x" ++ smallCharToHex c
   else String.singleton c
 where
@@ -383,7 +384,7 @@ Examples:
 -/
 def String.quote (s : String) : String :=
   if s.isEmpty then "\"\""
-  else s.foldl (fun s c => s ++ c.quoteCore) "\"" ++ "\""
+  else s.foldl (fun s c => s ++ c.quoteCore (inString := true)) "\"" ++ "\""
 
 instance : Repr String where
   reprPrec s _ := s.quote

tests/lean/run/charQuote.lean

@@ -0,0 +1,7 @@
+-- This used to delaborate as `'''`, which is a parse error.
+
+/--
+info: '\''
+-/
+#guard_msgs in
+#eval '\''