From 9b05f57ec861d6b05d910260036389e2035de67a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 18 Oct 2022 10:59:17 +0200
Subject: [PATCH] fix: wrap `&"..." <|> ...` as well

---
 src/Lean/Elab/Syntax.lean         | 11 +++++++----
 tests/lean/1275.lean              | 13 ++++++++++++-
 tests/lean/1275.lean.expected.out | 15 +++++++++++++--
 3 files changed, 32 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index e3e3968889..641f739e4a 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -166,10 +166,13 @@ where
     -- wrap lone string literals in `<|>` in dedicated node (#1275)
     let args' ← if aliasName == `orelse then  -- TODO: generalize if necessary
       args.zip args' |>.mapM fun (arg, arg') => do
-        if arg.getNumArgs == 1 && arg[0].isOfKind ``Lean.Parser.Syntax.atom then
-          if let some sym := arg[0][0].isStrLit? then
-            return (← `(ParserDescr.nodeWithAntiquot $(quote sym) $(quote (`token ++ sym)) $(arg'.1)), 1)
-        return arg'
+        let mut #[arg] := arg.getArgs | return arg'
+        let sym ← match arg with
+          | `(stx| &$sym) => pure sym
+          | `(stx| $sym:str) => pure sym
+          | _ => return arg'
+        let sym := sym.getString
+        return (← `(ParserDescr.nodeWithAntiquot $(quote sym) $(quote (`token ++ sym)) $(arg'.1)), 1)
     else
       pure args'
     let (args', stackSz) := if let some stackSz := info.stackSz? then
diff --git a/tests/lean/1275.lean b/tests/lean/1275.lean
index 8ba0efc505..1777a836f2 100644
--- a/tests/lean/1275.lean
+++ b/tests/lean/1275.lean
@@ -1,7 +1,7 @@
 import Lean open Lean
 
 syntax "👉" (ident <|> "_") : term
-#check `(👉 $_)
+#check fun x => `(👉 $x)
 #eval match Unhygienic.run `(👉 _) with
   | `(👉 $_:ident) => false
   | `(👉 _) => true
@@ -10,3 +10,14 @@ syntax "👉" (ident <|> "_") : term
   | `(👉 _) => false
   | `(👉 $_:ident) => true
   | _ => false
+
+syntax "bar" (&"baz" <|> &"boing") : term
+#check fun x => `(bar $x)
+#eval match Unhygienic.run `(bar boing) with
+  | `(bar baz) => false
+  | `(bar boing) => true
+  | _ => false
+#eval match Unhygienic.run `(bar baz) with
+  | `(bar boing) => false
+  | `(bar baz) => true
+  | _ => false
diff --git a/tests/lean/1275.lean.expected.out b/tests/lean/1275.lean.expected.out
index 54919d5a2b..68c627bcdb 100644
--- a/tests/lean/1275.lean.expected.out
+++ b/tests/lean/1275.lean.expected.out
@@ -1,9 +1,20 @@
-do
+fun x => do
   let info ← MonadRef.mkInfoFromRefPos
   let scp ← getCurrMacroScope
   let mainModule ← getMainModule
   pure
       { raw :=
-          Syntax.node2 info `term👉__ (Syntax.atom info "👉") (?m info scp mainModule).raw } : ?m (TSyntax `term)
+          Syntax.node2 info `term👉__ (Syntax.atom info "👉")
+            x.raw } : (x : TSyntax [`ident, `token._]) → ?m x (TSyntax `term)
+true
+true
+fun x => do
+  let info ← MonadRef.mkInfoFromRefPos
+  let scp ← getCurrMacroScope
+  let mainModule ← getMainModule
+  pure
+      { raw :=
+          Syntax.node2 info `termBarBazBoing (Syntax.atom info "bar")
+            x.raw } : (x : TSyntax [`token.baz, `token.boing]) → ?m x (TSyntax `term)
 true
 true