fix: quoting single quote Char (''')

[plp127]

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.

[nomeata]

LGTM, but I'll let someone from the library team press the button.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0002ea8a3702a0c2191b03e1274aefc05b53ca8c --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-12 15:39:59)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0002ea8a3702a0c2191b03e1274aefc05b53ca8c --onto faffe863343211d03d07d4ef19d90a2aa9d6fc8c. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-13 15:51:31)

[Rob23oba]

I feel like single quotes within double quotes or the other way round shouldn't need to escaped. Also (unrelated) the way it currently works is that it allocates a new string for every character when trying to quote, maybe we could instead use a function String.pushQuotedChar (s : String) (c : Char) (outerQuote : Char).

[Rob23oba]

So something like

def String.pushQuotedChar (s : String) (c : Char) (quote : Char := '"') : String :=
  if      c = '\n' then s.push '\\' |>.push 'n'
  else if c = '\t' then s.push '\\' |>.push 't'
  else if c = '\\' ∨ c = quote then s.push '\\' |>.push c
  else if c.toNat <= 31 ∨ c = '\x7f' then smallCharToHex s c
  else s.push c
where
  smallCharToHex (s : String) (c : Char) : String :=
    let n  := Char.toNat c
    let d2 := n / 16
    let d1 := n % 16
    s.push '\\' |>.push 'x' |>.push (Nat.digitChar d2) |>.push (Nat.digitChar d1)

As Rob says, the change to string literals is probably not great.