diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index b8fb5f2801aa..3c2854684bce 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -271,10 +271,11 @@ abbrev CharLit := TSyntax charLitKind
 abbrev NameLit := TSyntax nameLitKind
 abbrev ScientificLit := TSyntax scientificLitKind
 abbrev NumLit := TSyntax numLitKind
+abbrev HygieneInfo := TSyntax hygieneInfoKind
 
 end Syntax
 
-export Syntax (Term Command Prec Prio Ident StrLit CharLit NameLit ScientificLit NumLit)
+export Syntax (Term Command Prec Prio Ident StrLit CharLit NameLit ScientificLit NumLit HygieneInfo)
 
 namespace TSyntax
 
@@ -921,6 +922,9 @@ def getChar (s : CharLit) : Char :=
 def getName (s : NameLit) : Name :=
   s.raw.isNameLit?.getD .anonymous
 
+def getHygieneInfo (s : HygieneInfo) : Name :=
+  s.raw[0].getId
+
 namespace Compat
 
 scoped instance : CoeTail (Array Syntax) (Syntax.TSepArray k sep) where
@@ -930,6 +934,11 @@ end Compat
 
 end TSyntax
 
+def HygieneInfo.mkIdent (s : HygieneInfo) (val : Name) (canonical := false) : Ident :=
+  let src := s.raw[0]
+  let id := { extractMacroScopes src.getId with name := val.eraseMacroScopes }.review
+  ⟨Syntax.ident (SourceInfo.fromRef src canonical) (toString val).toSubstring id []⟩
+
 /-- Reflect a runtime datum back to surface syntax (best-effort). -/
 class Quote (α : Type) (k : SyntaxNodeKind := `term) where
   quote : α → TSyntax k
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index be52954b44af..c3bb42d9bb9d 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -3721,6 +3721,16 @@ abbrev nameLitKind : SyntaxNodeKind := `name
 /-- `fieldIdx` is the node kind of projection indices like the `2` in `x.2`. -/
 abbrev fieldIdxKind : SyntaxNodeKind := `fieldIdx
 
+/--
+`hygieneInfo` is the node kind of the `hygieneInfo` parser, which is an
+"invisible token" which captures the hygiene information at the current point
+without parsing anything.
+
+They can be used to generate identifiers (with `Lean.HygieneInfo.mkIdent`)
+as if they were introduced by the calling context, not the called macro.
+-/
+abbrev hygieneInfoKind : SyntaxNodeKind := `hygieneInfo
+
 /--
 `interpolatedStrLitKind` is the node kind of interpolated string literal
 fragments like `"value = {` and `}"` in `s!"value = {x}"`.
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 165c8e46631d..0e231ddfb87f 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -260,7 +260,7 @@ open Lean.Parser.Command
 
 private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
   if let .str _ suffix := catName then
-    let quotSymbol := "`(" ++ suffix ++ "|"
+    let quotSymbol := "`(" ++ suffix ++ "| "
     let name := catName ++ `quot
     let cmd ← `(
       @[term_parser] def $(mkIdent name) : Lean.ParserDescr :=
diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean
index 8b3683a99885..7745db80ed20 100644
--- a/src/Lean/Parser.lean
+++ b/src/Lean/Parser.lean
@@ -27,7 +27,8 @@ builtin_initialize
   register_parser_alias (kind := charLitKind) "char" charLit
   register_parser_alias (kind := nameLitKind) "name" nameLit
   register_parser_alias (kind := scientificLitKind) "scientific" scientificLit
-  register_parser_alias (kind := identKind) "ident" ident
+  register_parser_alias (kind := identKind) ident
+  register_parser_alias (kind := hygieneInfoKind) hygieneInfo
   register_parser_alias "colGt" checkColGt { stackSz? := some 0 }
   register_parser_alias "colGe" checkColGe { stackSz? := some 0 }
   register_parser_alias "colEq" checkColEq { stackSz? := some 0 }
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 0eb426b3ad19..e7eef8967dd4 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1072,6 +1072,20 @@ def identEq (id : Name) : Parser := {
   info := mkAtomicInfo "ident"
 }
 
+def hygieneInfoFn : ParserFn := fun c s =>
+  let input := c.input
+  let pos   := s.pos
+  let str   := mkEmptySubstringAt input pos
+  let info  := SourceInfo.original str pos str pos
+  let ident := mkIdent info str .anonymous
+  let stx   := mkNode hygieneInfoKind #[ident]
+  s.pushSyntax stx
+
+def hygieneInfoNoAntiquot : Parser := {
+  fn   := hygieneInfoFn
+  info := nodeInfo hygieneInfoKind epsilonInfo
+}
+
 namespace ParserState
 
 def keepTop (s : SyntaxStack) (startStackSize : Nat) : SyntaxStack :=
diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean
index 10817d1e3239..a00944f6f648 100644
--- a/src/Lean/Parser/Extra.lean
+++ b/src/Lean/Parser/Extra.lean
@@ -37,6 +37,9 @@ attribute [run_builtin_parser_attribute_hooks]
 @[run_builtin_parser_attribute_hooks] def rawIdent : Parser :=
   withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot
 
+@[run_builtin_parser_attribute_hooks] def hygieneInfo : Parser :=
+  withAntiquot (mkAntiquot "hygieneInfo" hygieneInfoKind (anonymous := false)) hygieneInfoNoAntiquot
+
 @[run_builtin_parser_attribute_hooks] def numLit : Parser :=
   withAntiquot (mkAntiquot "num" numLitKind) numLitNoAntiquot
 
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 2f9beb8f60dd..da8effa217f0 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -489,6 +489,7 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
 @[combinator_formatter skip] def skip.formatter : Formatter := pure ()
 
 @[combinator_formatter pushNone] def pushNone.formatter : Formatter := goLeft
+@[combinator_formatter hygieneInfoNoAntiquot] def hygieneInfoNoAntiquot.formatter : Formatter := goLeft
 
 @[combinator_formatter interpolatedStr]
 def interpolatedStr.formatter (p : Formatter) : Formatter := do
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 988905f76529..b007273b652b 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -492,6 +492,7 @@ def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
 @[combinator_parenthesizer skip] def skip.parenthesizer : Parenthesizer := pure ()
 
 @[combinator_parenthesizer pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft
+@[combinator_parenthesizer hygieneInfoNoAntiquot] def hygieneInfoNoAntiquot.parenthesizer : Parenthesizer := goLeft
 
 @[combinator_parenthesizer interpolatedStr]
 def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do
diff --git a/tests/lean/interactive/1265.lean.expected.out b/tests/lean/interactive/1265.lean.expected.out
index bf1c2fa6a2cd..787c3640f3f8 100644
--- a/tests/lean/interactive/1265.lean.expected.out
+++ b/tests/lean/interactive/1265.lean.expected.out
@@ -1,7 +1,10 @@
 {"textDocument": {"uri": "file://1265.lean"},
  "position": {"line": 0, "character": 51}}
 {"items":
- [{"label": "getId", "kind": 3, "detail": "Lean.Ident → Lean.Name"},
+ [{"label": "getHygieneInfo",
+   "kind": 3,
+   "detail": "Lean.HygieneInfo → Lean.Name"},
+  {"label": "getId", "kind": 3, "detail": "Lean.Ident → Lean.Name"},
   {"label": "getName", "kind": 3, "detail": "Lean.NameLit → Lean.Name"},
   {"label": "expandInterpolatedStr",
    "kind": 3,
@@ -22,7 +25,10 @@
 {"textDocument": {"uri": "file://1265.lean"},
  "position": {"line": 2, "character": 53}}
 {"items":
- [{"label": "getId", "kind": 3, "detail": "Lean.Ident → Lean.Name"},
+ [{"label": "getHygieneInfo",
+   "kind": 3,
+   "detail": "Lean.HygieneInfo → Lean.Name"},
+  {"label": "getId", "kind": 3, "detail": "Lean.Ident → Lean.Name"},
   {"label": "getName", "kind": 3, "detail": "Lean.NameLit → Lean.Name"},
   {"label": "expandInterpolatedStr",
    "kind": 3,