fix: wrap &"..." <|> ... as well

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

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

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