Make tokens in <|> relevant to syntax match

src/Init/Conv.lean

@@ -227,7 +227,7 @@ resulting in `t'`, which becomes the new target subgoal. -/
 syntax (name := convConvSeq) "conv" " => " convSeq : conv
 
 /-- `· conv` focuses on the main conv goal and tries to solve it using `s`. -/
-macro dot:("·" <|> ".") s:convSeq : conv => `(conv| {%$dot ($s) })
+macro dot:patternIgnore("·" <|> ".") s:convSeq : conv => `(conv| {%$dot ($s) })
 
 
 /-- `fail_if_success t` fails if the tactic `t` succeeds. -/

src/Init/NotationExtra.lean

@@ -61,10 +61,10 @@ def expandBrackedBinders (combinatorDeclName : Name) (bracketedExplicitBinders :
   let combinator := mkIdentFrom (← getRef) combinatorDeclName
   expandBrackedBindersAux combinator #[bracketedExplicitBinders] body
 
-syntax unifConstraint := term (" =?= " <|> " ≟ ") term
+syntax unifConstraint := term patternIgnore(" =?= " <|> " ≟ ") term
 syntax unifConstraintElem := colGe unifConstraint ", "?
 
-syntax (docComment)? attrKind "unif_hint " (ident)? bracketedBinder* " where " withPosition(unifConstraintElem*) ("|-" <|> "⊢ ") unifConstraint : command
+syntax (docComment)? attrKind "unif_hint " (ident)? bracketedBinder* " where " withPosition(unifConstraintElem*) patternIgnore("|-" <|> "⊢ ") unifConstraint : command
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁ ≟ $cs₂]* |- $t₁ ≟ $t₂) => do
@@ -337,14 +337,15 @@ macro_rules
 
 section
 open Lean.Parser.Tactic
+syntax cdotTk := patternIgnore("·" <|> ".")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
-syntax ("·" <|> ".") ppHardSpace many1Indent(tactic ";"? ppLine) : tactic
+syntax cdotTk ppHardSpace many1Indent(tactic ";"? ppLine) : tactic
 macro_rules
-  | `(tactic| ·%$dot $[$tacs $[;%$sc]?]*) => do
+  | `(tactic| $cdot:cdotTk $[$tacs $[;%$sc]?]*) => do
     let tacs ← tacs.zip sc |>.mapM fun
       | (tac, none)    => pure tac
       | (tac, some sc) => `(tactic| ($tac; with_annotate_state $sc skip))
-    `(tactic| { with_annotate_state $dot skip; $[$tacs]* })
+    `(tactic| { with_annotate_state $cdot skip; $[$tacs]* })
 end
 
 /--

src/Init/Tactics.lean

@@ -304,7 +304,7 @@ syntax locationWildcard := "*"
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
-syntax locationHyp := (colGt term:max)+ ("⊢" <|> "|-")?
+syntax locationHyp := (colGt term:max)+ patternIgnore("⊢" <|> "|-")?
 
 /--
 Location specifications are used by many tactics that can operate on either the
@@ -337,7 +337,7 @@ If `thm` is a theorem `a = b`, then as a rewrite rule,
 * `thm` means to replace `a` with `b`, and
 * `← thm` means to replace `b` with `a`.
 -/
-syntax rwRule    := ("← " <|> "<- ")? term
+syntax rwRule    := patternIgnore("← " <|> "<- ")? term
 /-- A `rwRuleSeq` is a list of `rwRule` in brackets. -/
 syntax rwRuleSeq := " [" withoutPosition(rwRule,*,?) "]"
 
@@ -388,7 +388,7 @@ syntax (name := injections) "injections" (colGt (ident <|> hole))* : tactic
 The discharger clause of `simp` and related tactics.
 This is a tactic used to discharge the side conditions on conditional rewrite rules.
 -/
-syntax discharger := atomic(" (" (&"discharger" <|> &"disch")) " := " withoutPosition(tacticSeq) ")"
+syntax discharger := atomic(" (" patternIgnore(&"discharger" <|> &"disch")) " := " withoutPosition(tacticSeq) ")"
 
 /-- Use this rewrite rule before entering the subterms -/
 syntax simpPre   := "↓"
@@ -400,7 +400,7 @@ A simp lemma specification is:
 * optional `←` to use the lemma backward
 * `thm` for the theorem to rewrite with
 -/
-syntax simpLemma := (simpPre <|> simpPost)? ("← " <|> "<- ")? term
+syntax simpLemma := (simpPre <|> simpPost)? patternIgnore("← " <|> "<- ")? term
 /-- An erasure specification `-thm` says to remove `thm` from the simp set -/
 syntax simpErase := "-" term:max
 /-- The simp lemma specification `*` means to rewrite with all hypotheses -/

src/Lean/Elab/Quotation.lean

@@ -340,7 +340,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
     if let some (k, _) := quoted.antiquotKind? then
       if let some name := getAntiquotKindSpec? quoted then
         tryAddSyntaxNodeKindInfo name k
-    if quoted.isAtom then
+    if quoted.isAtom || quoted.isOfKind `patternIgnore then
       -- We assume that atoms are uniquely determined by the node kind and never have to be checked
       unconditionally pure
     else if quoted.isTokenAntiquot then

src/Lean/Elab/Syntax.lean

@@ -162,16 +162,28 @@ where
     let aliasName := id.getId.eraseMacroScopes
     let info ← Parser.getParserAliasInfo aliasName
     addAliasInfo id info
-    let args ← args.mapM (withNestedParser ∘ process)
-    let (args, stackSz) := if let some stackSz := info.stackSz? then
+    let args' ← args.mapM (withNestedParser ∘ process)
+    -- 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
+        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
       if !info.autoGroupArgs then
-        (args.map (·.1), stackSz)
+        (args'.map (·.1), stackSz)
       else
-        (args.map ensureUnaryOutput, stackSz)
+        (args'.map ensureUnaryOutput, stackSz)
     else
-      let (args, stackSzs) := args.unzip
-      (args, stackSzs.foldl (· + ·) 0)
-    let stx ← match args with
+      let (args', stackSzs) := args'.unzip
+      (args', stackSzs.foldl (· + ·) 0)
+    let stx ← match args' with
       | #[]       => Parser.ensureConstantParserAlias aliasName; ``(ParserDescr.const $(quote aliasName))
       | #[p1]     => Parser.ensureUnaryParserAlias aliasName; ``(ParserDescr.unary $(quote aliasName) $p1)
       | #[p1, p2] => Parser.ensureBinaryParserAlias aliasName; ``(ParserDescr.binary $(quote aliasName) $p1 $p2)

src/Lean/Parser.lean

@@ -76,7 +76,8 @@ unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer
   | ParserDescr.unary n d                           => return (← getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d)
   | ParserDescr.binary n d₁ d₂                      => return (← getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂)
   | ParserDescr.node k prec d                       => return leadingNode.parenthesizer k prec (← interpretParserDescr d)
-  | ParserDescr.nodeWithAntiquot _ k d              => return node.parenthesizer k (← interpretParserDescr d)
+  | ParserDescr.nodeWithAntiquot n k d              => return withAntiquot.parenthesizer (mkAntiquot.parenthesizer' n k (anonymous := true)) <|
+                                                                node.parenthesizer k (← interpretParserDescr d)
   | ParserDescr.sepBy p sep psep trail              => return sepBy.parenthesizer (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
   | ParserDescr.sepBy1 p sep psep trail             => return sepBy1.parenthesizer (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
   | ParserDescr.trailingNode k prec lhsPrec d       => return trailingNode.parenthesizer k prec lhsPrec (← interpretParserDescr d)
@@ -107,7 +108,8 @@ unsafe def interpretParserDescr : ParserDescr → CoreM Formatter
   | ParserDescr.unary n d                           => return (← getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d)
   | ParserDescr.binary n d₁ d₂                      => return (← getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂)
   | ParserDescr.node k _ d                          => return node.formatter k (← interpretParserDescr d)
-  | ParserDescr.nodeWithAntiquot _ k d              => return node.formatter k (← interpretParserDescr d)
+  | ParserDescr.nodeWithAntiquot n k d              => return withAntiquot.formatter (mkAntiquot.formatter' n k (anonymous := true)) <|
+                                                                node.formatter k (← interpretParserDescr d)
   | ParserDescr.sepBy p sep psep trail              => return sepBy.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
   | ParserDescr.sepBy1 p sep psep trail             => return sepBy1.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
   | ParserDescr.trailingNode k prec lhsPrec d       => return trailingNode.formatter k prec lhsPrec (← interpretParserDescr d)

src/Lean/Parser/Extra.lean

@@ -89,6 +89,9 @@ attribute [run_builtin_parser_attribute_hooks] sepByIndent sepBy1Indent
 @[run_builtin_parser_attribute_hooks] abbrev notSymbol (s : String) : Parser :=
   notFollowedBy (symbol s) s
 
+/-- No-op parser combinator that annotates subtrees to be ignored in syntax patterns. -/
+@[inline, run_builtin_parser_attribute_hooks] def patternIgnore : Parser → Parser := node `patternIgnore
+
 /-- No-op parser that advises the pretty printer to emit a non-breaking space. -/
 @[inline] def ppHardSpace : Parser := skip
 /-- No-op parser that advises the pretty printer to emit a space/soft line break. -/
@@ -182,6 +185,8 @@ macro_rules
          PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer)))
 
 builtin_initialize
+  register_parser_alias patternIgnore { autoGroupArgs := false }
+
   register_parser_alias group { autoGroupArgs := false }
   register_parser_alias ppHardSpace { stackSz? := some 0 }
   register_parser_alias ppSpace { stackSz? := some 0 }

src/Lean/PrettyPrinter/Formatter.lean

@@ -173,10 +173,18 @@ def withMaybeTag (pos? : Option String.Pos) (x : FormatterM Unit) : Formatter :=
   else
     x
 
-@[combinator_formatter orelse] def orelse.formatter (p1 p2 : Formatter) : Formatter :=
-  -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
-  -- them in turn. Uses the syntax traverser non-linearly!
-  p1 <|> p2
+@[combinator_formatter orelse] partial def orelse.formatter (p1 p2 : Formatter) : Formatter := do
+  let stx ← getCur
+  -- `orelse` may produce `choice` nodes for antiquotations
+  if stx.getKind == `choice then
+    visitArgs do
+      -- format only last choice
+      -- TODO: We could use elaborator data here to format the chosen child when available
+      orelse.formatter p1 p2
+  else
+    -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
+    -- them in turn. Uses the syntax traverser non-linearly!
+    p1 <|> p2
 
 -- `mkAntiquot` is quite complex, so we'd rather have its formatter synthesized below the actual parser definition.
 -- Note that there is a mutual recursion

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -247,10 +247,16 @@ def visitToken : Parenthesizer := do
   modify fun st => { st with contPrec := none, contCat := Name.anonymous, visitedToken := true }
   goLeft
 
-@[combinator_parenthesizer orelse] def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do
-  -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
-  -- them in turn. Uses the syntax traverser non-linearly!
-  p1 <|> p2
+@[combinator_parenthesizer orelse] partial def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do
+  let stx ← getCur
+  -- `orelse` may produce `choice` nodes for antiquotations
+  if stx.getKind == `choice then
+    visitArgs $ stx.getArgs.size.forM fun _ => do
+      orelse.parenthesizer p1 p2
+  else
+    -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
+    -- them in turn. Uses the syntax traverser non-linearly!
+    p1 <|> p2
 
 -- `mkAntiquot` is quite complex, so we'd rather have its parenthesizer synthesized below the actual parser definition.
 -- Note that there is a mutual recursion
@@ -299,13 +305,12 @@ def tokenWithAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do
   else
     p
 
-def parenthesizeCategoryCore (cat : Name) (_prec : Nat) : Parenthesizer :=
+partial def parenthesizeCategoryCore (cat : Name) (_prec : Nat) : Parenthesizer :=
   withReader (fun ctx => { ctx with cat := cat }) do
     let stx ← getCur
     if stx.getKind == `choice then
       visitArgs $ stx.getArgs.size.forM fun _ => do
-        let stx ← getCur
-        parenthesizerForKind stx.getKind
+        parenthesizeCategoryCore cat _prec
     else
       withAntiquot.parenthesizer (mkAntiquot.parenthesizer' cat.toString cat (isPseudoKind := true)) (parenthesizerForKind stx.getKind)
     modify fun st => { st with contCat := cat }