fix: make formatter use current token table (#5389)

Previously the formatter was using the builtin token table rather that
the one in the current environment. This could lead to round-tripping
failures for user-defined notations.

For an illustrative example, given the following notation
```lean
infixl:65 "+'" => Int.add
notation:65 a:65 "+'-" b:66 => Int.add a (id b)
```
then `5 +' -1` would parse as `Int.add 5 (-1)` and incorrectly pretty
print as `5+'-1`, which in turn would parse as `Int.add 5 (id 1)`. Now
it pretty prints as `5+' -1`.

src/Lean/PrettyPrinter/Formatter.lean

@@ -420,8 +420,8 @@ def identNoAntiquot.formatter : Formatter := do
   let stx@(Syntax.ident info _ id _) ← getCur
     | throwError m!"not an ident: {← getCur}"
   let id := id.simpMacroScopes
-  let tokenTable := getTokenTable (← getEnv)
-  let isToken (s : String) : Bool := (tokenTable.find? s).isSome
+  let table := (← read).table
+  let isToken (s : String) : Bool := (table.find? s).isSome
   withMaybeTag (getExprPos? stx) (pushToken info (id.toString (isToken := isToken)))
   goLeft
 
@@ -537,7 +537,7 @@ register_builtin_option pp.oneline : Bool := {
 def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do
   trace[PrettyPrinter.format.input] "{Std.format stx}"
   let options ← getOptions
-  let table ← Parser.builtinTokenTable.get
+  let table := Parser.getTokenTable (← getEnv)
   catchInternalId backtrackExceptionId
     (do
       let (_, st) ← (concat formatter { table, options }).run { stxTrav := .fromSyntax stx }

tests/lean/run/formatterTokenTable.lean

@@ -0,0 +1,16 @@
+/-!
+# Verify that the formatter uses the current token table
+
+Formerly, the formatter was only looking at the builtin token table
+when deciding where to insert additional whitespace between tokens.
+This lead to `5+' -1` in the following pretty printing as `5+'-1`.
+-/
+
+infixl:65 "+'" => Int.add
+notation:65 a:65 "+'-" b:66 => Int.add a (id b)
+
+/-- info: 5+' -1 : Int -/
+#guard_msgs in #check 5 +' -1
+
+/-- info: 5+'-1 : Int -/
+#guard_msgs in #check 5 +'- 1