fix: keep the space before a hygieneInfo antiquotation

src/Lean/Parser/Basic.lean

@@ -1888,6 +1888,17 @@ def withAntiquotFn (antiquotP p : ParserFn) (isCatAntiquot := false) : ParserFn
   info := orelseInfo antiquotP.info p.info
 }
 
+/--
+Like `withAntiquot`, but uses `OrElseOnAntiquotBehavior.acceptLhs` instead of `.takeLongest`.
+This means that when the antiquotation parser `antiquotP` succeeds, `p` is not tried.
+This is useful when `p` has side effects on the parser stack that would not be undone by
+backtracking.
+-/
+@[builtin_doc] def withAntiquotAcceptLhs (antiquotP p : Parser) : Parser := {
+  fn := withAntiquotFn antiquotP.fn p.fn (isCatAntiquot := true)
+  info := orelseInfo antiquotP.info p.info
+}
+
 def withoutInfo (p : Parser) : Parser := {
   fn := p.fn
 }

src/Lean/Parser/Extra.lean

@@ -108,7 +108,13 @@ This parser has arity 1: it produces a `hygieneInfoKind` node containing an anon
 You can use `HygieneInfo.mkIdent` to create an `Ident` from the syntax object,
 but you can also use `TSyntax.getHygieneInfo` to get the raw name from the identifier. -/
 @[run_builtin_parser_attribute_hooks, builtin_doc] def hygieneInfo : Parser :=
-  withAntiquot (mkAntiquot "hygieneInfo" hygieneInfoKind (anonymous := false)) hygieneInfoNoAntiquot
+  -- We cannot use `withAntiquot` here because it uses `OrElseOnAntiquotBehavior.takeLongest`,
+  -- meaning that `hygieneInfoFn` would also be run when the antiquotation parser succeeds.
+  -- `hygieneInfoFn` has a side effect on the previous token in the parser stack that survives
+  -- backtracking: it steals trailing whitespace from the previous token.
+  -- This side effect must not occur when the antiquotation parser already succeeded, since the
+  -- antiquotation will always parse further than the zero-width `hygieneInfoFn`.
+  withAntiquotAcceptLhs (mkAntiquot "hygieneInfo" hygieneInfoKind (anonymous := false)) hygieneInfoNoAntiquot
 
 /-- The parser `num` parses a numeric literal in several bases:
 

src/Lean/PrettyPrinter/Formatter.lean

@@ -265,7 +265,7 @@ unsafe def formatterForKindUnsafe (k : SyntaxNodeKind) : Formatter := do
 @[implemented_by formatterForKindUnsafe]
 opaque formatterForKind (k : SyntaxNodeKind) : Formatter
 
-@[combinator_formatter withAntiquot, expose]
+@[combinator_formatter withAntiquot, combinator_formatter withAntiquotAcceptLhs, expose]
 def withAntiquot.formatter (antiP p : Formatter) : Formatter :=
   -- TODO: could be optimized using `isAntiquot` (which would have to be moved), but I'd rather
   -- fix the backtracking hack outright.

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -329,7 +329,7 @@ unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do
 @[implemented_by parenthesizerForKindUnsafe]
 opaque parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer
 
-@[combinator_parenthesizer withAntiquot, expose]
+@[combinator_parenthesizer withAntiquot, combinator_parenthesizer withAntiquotAcceptLhs, expose]
 def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer := do
   let stx ← getCur
   -- early check as minor optimization that also cleans up the backtrack traces

tests/elab/hygieneInfoAntiquot.lean

@@ -0,0 +1,39 @@
+import Lean
+
+/-!
+# `hygieneInfo` antiquotations keep the preceding token's trailing whitespace
+
+`hygieneInfoFn` moves the previous token's trailing whitespace onto the `hygieneInfo` node it
+produces. That edit reaches below its own stack frame, so it is not undone by backtracking. When a
+`hygieneInfo` antiquotation matched, `withAntiquot` used to run `hygieneInfoFn` as well and then
+throw its result away, and the whitespace went with it.
+-/
+
+open Lean
+
+elab "#reprint " s:str : command => Elab.Command.liftTermElabM do
+  let stx ← ofExcept <| Parser.runParserCategory (← getEnv) `term s.getString
+  logInfo s!"‹{stx.reprint.getD "<reprint failed>"}›"
+
+/-!
+A `hygieneInfo` antiquotation after `·`. The space after `·` used to disappear.
+-/
+/-- info: ‹`(· $h:hygieneInfo)› -/
+#guard_msgs in #reprint "`(· $h:hygieneInfo)"
+
+/-!
+The same for the other parsers that follow a token with `hygieneInfo`: `(` in `hygienicLParen`,
+and `suffices`.
+-/
+/-- info: ‹`(( $h:hygieneInfo x))› -/
+#guard_msgs in #reprint "`(( $h:hygieneInfo x))"
+
+/-- info: ‹`(suffices $h:hygieneInfo p from q; r)› -/
+#guard_msgs in #reprint "`(suffices $h:hygieneInfo p from q; r)"
+
+/-!
+Without an antiquotation `hygieneInfoFn` still runs, and reprinting is unaffected: the whitespace
+only moves from `·` onto the `hygieneInfo` node.
+-/
+/-- info: ‹(· + 1)› -/
+#guard_msgs in #reprint "(· + 1)"