refactor: split paren parser, part 2

src/Lean/Parser/Term.lean

@@ -128,27 +128,28 @@ For example, `(· + ·)` is equivalent to `fun x y => x + y`.
 -/
 @[builtin_term_parser] def cdot   := leading_parser
   symbol "·" <|> "."
-def typeAscription := leading_parser
-  "(" >> withoutPosition (withoutForbidden (termParser >> " : " >> optional termParser)) >> ")"
-def tuple := leading_parser
+/--
+Type ascription notation: `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
+An empty type ascription `(e :)` elaborates `e` without the expected type.
+This is occasionally useful when Lean's heuristics for filling arguments from the expected type
+do not yield the right result.
+-/
+@[builtin_term_parser] def typeAscription := leading_parser
+  "(" >> (withoutPosition (withoutForbidden (termParser >> " : " >> optional termParser))) >> ")"
+/-- Tuple notation; `()` is short for `Unit.unit`, `(a, b, c)` for `Prod.mk a (Prod.mk b c)`, etc. -/
+@[builtin_term_parser] def tuple := leading_parser
   "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", "))) >> ")"
 /--
-Parentheses, used for
-- Grouping expressions, e.g., `a * (b + c)`.
-- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.
-- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
-  - An empty type ascription `(e :)` elaborates `e` without the expected type.
-    This is occasionally useful when Lean's heuristics for filling arguments from the expected type
-    do not yield the right result.
-- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.
-- Creating simple functions when combined with `·`. Here are some examples:
+Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
+Can also be used for creating simple functions when combined with `·`. Here are some examples:
   - `(· + 1)` is shorthand for `fun x => x + 1`
   - `(· + ·)` is shorthand for `fun x y => x + y`
   - `(f · a b)` is shorthand for `fun x => f x a b`
   - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
+  - also applies to other parentheses-like notations such as `(·, 1)`
 -/
-@[builtin_term_parser] def paren := (leading_parser
-  atomic ("(" >> withoutPosition (withoutForbidden (ppDedentIfGrouped termParser)) >> ")")) <|> atomic typeAscription <|> tuple
+@[builtin_term_parser] def paren := leading_parser
+  "(" >> withoutPosition (withoutForbidden (ppDedentIfGrouped termParser)) >> ")"
 /--
 The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
 expected type is an inductive type with a single constructor `c`.

tests/lean/StxQuot.lean.expected.out

@@ -24,8 +24,8 @@ StxQuot.lean:19:15: error: expected term
 0
 1
 "1"
-"(Term.fun\n \"fun\"\n (Term.basicFun\n  [`a._@.UnhygienicMain._hyg.1\n   (Term.paren \"(\" [`b._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" [`Nat._@.UnhygienicMain._hyg.1])]] \")\")]\n  []\n  \"=>\"\n  (num \"1\")))"
-"#[(Term.paren \"(\" [`a._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" [`Nat._@.UnhygienicMain._hyg.1])]] \")\"), `b._@.UnhygienicMain._hyg.1]"
+"(Term.fun\n \"fun\"\n (Term.basicFun\n  [`a._@.UnhygienicMain._hyg.1\n   (Term.typeAscription \"(\" `b._@.UnhygienicMain._hyg.1 \":\" [`Nat._@.UnhygienicMain._hyg.1] \")\")]\n  []\n  \"=>\"\n  (num \"1\")))"
+"#[(Term.typeAscription \"(\" `a._@.UnhygienicMain._hyg.1 \":\" [`Nat._@.UnhygienicMain._hyg.1] \")\"), `b._@.UnhygienicMain._hyg.1]"
 "`a._@.UnhygienicMain._hyg.1"
 "(Term.forall \"∀\" [(Term.hole \"_\")] [] \",\" `c._@.UnhygienicMain._hyg.1)"
 "(Term.hole \"_\")"

tests/lean/interactive/hover.lean.expected.out

@@ -387,7 +387,7 @@ null
   "end": {"line": 201, "character": 32}},
  "contents":
  {"value":
-  "```lean\nId ℕ\n```\n***\nParentheses, used for\n- Grouping expressions, e.g., `a * (b + c)`.\n- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.\n- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.\n  - An empty type ascription `(e :)` elaborates `e` without the expected type.\n    This is occasionally useful when Lean's heuristics for filling arguments from the expected type\n    do not yield the right result.\n- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.\n- Creating simple functions when combined with `·`. Here are some examples:\n  - `(· + 1)` is shorthand for `fun x => x + 1`\n  - `(· + ·)` is shorthand for `fun x y => x + y`\n  - `(f · a b)` is shorthand for `fun x => f x a b`\n  - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`\n",
+  "```lean\nId ℕ\n```\n***\nParentheses, used for grouping expressions (e.g., `a * (b + c)`).\nCan also be used for creating simple functions when combined with `·`. Here are some examples:\n  - `(· + 1)` is shorthand for `fun x => x + 1`\n  - `(· + ·)` is shorthand for `fun x y => x + y`\n  - `(f · a b)` is shorthand for `fun x => f x a b`\n  - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`\n  - also applies to other parentheses-like notations such as `(·, 1)`\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 204, "character": 8}}