From 10061e8e3cfddd8834804dc496360aeb73ba115b Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Fri, 19 Apr 2024 07:42:34 -0400
Subject: [PATCH 1/3] feat: @[builtin_doc] attribute (part 2)

---
 src/Lean/Parser/Basic.lean            | 46 ++++++++++----------
 src/Lean/Parser/Command.lean          | 22 ++++++----
 src/Lean/Parser/Do.lean               |  2 +-
 src/Lean/Parser/Extra.lean            | 61 ++++++++++++++-------------
 src/Lean/Parser/StrInterpolation.lean |  2 +-
 src/Lean/Parser/Term.lean             | 44 ++++++++++---------
 src/Lean/Parser/Types.lean            |  3 +-
 7 files changed, 94 insertions(+), 86 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 7ba45f62a652..dc1ec8f13946 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -145,7 +145,7 @@ def errorAtSavedPosFn (msg : String) (delta : Bool) : ParserFn := fun c s =>
 /-- Generate an error at the position saved with the `withPosition` combinator.
    If `delta == true`, then it reports at saved position+1.
    This useful to make sure a parser consumed at least one character.  -/
-def errorAtSavedPos (msg : String) (delta : Bool) : Parser := {
+@[builtin_doc] def errorAtSavedPos (msg : String) (delta : Bool) : Parser := {
   fn := errorAtSavedPosFn msg delta
 }
 
@@ -271,7 +271,7 @@ def orelseFn (p q : ParserFn) : ParserFn :=
   NOTE: In order for the pretty printer to retrace an `orelse`, `p` must be a call to `node` or some other parser
   producing a single node kind. Nested `orelse` calls are flattened for this, i.e. `(node k1 p1 <|> node k2 p2) <|> ...`
   is fine as well. -/
-def orelse (p q : Parser) : Parser where
+@[builtin_doc] def orelse (p q : Parser) : Parser where
   info := orelseInfo p.info q.info
   fn   := orelseFn p.fn q.fn
 
@@ -295,7 +295,7 @@ This is important for the `p <|> q` combinator, because it is not backtracking,
 `p` fails after consuming some tokens. To get backtracking behavior, use `atomic(p) <|> q` instead.
 
 This parser has the same arity as `p` - it produces the same result as `p`. -/
-def atomic : Parser → Parser := withFn atomicFn
+@[builtin_doc] def atomic : Parser → Parser := withFn atomicFn
 
 /-- Information about the state of the parse prior to the failing parser's execution -/
 structure RecoveryContext where
@@ -335,7 +335,7 @@ state immediately after the failure.
 
 The interactions between <|> and `recover'` are subtle, especially for syntactic
 categories that admit user extension. Consider avoiding it in these cases. -/
-def recover' (parser : Parser) (handler : RecoveryContext → Parser) : Parser where
+@[builtin_doc] def recover' (parser : Parser) (handler : RecoveryContext → Parser) : Parser where
   info := parser.info
   fn := recoverFn parser.fn fun s => handler s |>.fn
 
@@ -347,7 +347,7 @@ If `handler` fails itself, then no recovery is performed.
 
 The interactions between <|> and `recover` are subtle, especially for syntactic
 categories that admit user extension. Consider avoiding it in these cases. -/
-def recover (parser handler : Parser) : Parser := recover' parser fun _ => handler
+@[builtin_doc] def recover (parser handler : Parser) : Parser := recover' parser fun _ => handler
 
 def optionalFn (p : ParserFn) : ParserFn := fun c s =>
   let iniSz  := s.stackSize
@@ -378,7 +378,7 @@ position to the original state on success. So for example `lookahead("=>")` will
 next token is `"=>"`, without actually consuming this token.
 
 This parser has arity 0 - it does not capture anything. -/
-def lookahead : Parser → Parser := withFn lookaheadFn
+@[builtin_doc] def lookahead : Parser → Parser := withFn lookaheadFn
 
 def notFollowedByFn (p : ParserFn) (msg : String) : ParserFn := fun c s =>
   let iniSz  := s.stackSize
@@ -394,7 +394,7 @@ def notFollowedByFn (p : ParserFn) (msg : String) : ParserFn := fun c s =>
 if `p` succeeds then it fails with the message `"unexpected foo"`.
 
 This parser has arity 0 - it does not capture anything. -/
-def notFollowedBy (p : Parser) (msg : String) : Parser where
+@[builtin_doc] def notFollowedBy (p : Parser) (msg : String) : Parser where
   fn := notFollowedByFn p.fn msg
 
 partial def manyAux (p : ParserFn) : ParserFn := fun c s => Id.run do
@@ -1146,7 +1146,7 @@ def checkWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
 For example, the parser `"foo" ws "+"` parses `foo +` or `foo/- -/+` but not `foo+`.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkWsBefore (errorMsg : String := "space before") : Parser where
+@[builtin_doc] def checkWsBefore (errorMsg : String := "space before") : Parser where
   info := epsilonInfo
   fn   := checkWsBeforeFn errorMsg
 
@@ -1163,7 +1163,7 @@ def checkLinebreakBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
 (The line break may be inside a comment.)
 
 This parser has arity 0 - it does not capture anything. -/
-def checkLinebreakBefore (errorMsg : String := "line break") : Parser where
+@[builtin_doc] def checkLinebreakBefore (errorMsg : String := "line break") : Parser where
   info := epsilonInfo
   fn   := checkLinebreakBeforeFn errorMsg
 
@@ -1183,7 +1183,7 @@ This is almost the same as `"foo+"`, but using this parser will make `foo+` a to
 problems for the use of `"foo"` and `"+"` as separate tokens in other parsers.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkNoWsBefore (errorMsg : String := "no space before") : Parser := {
+@[builtin_doc] def checkNoWsBefore (errorMsg : String := "no space before") : Parser := {
   info := epsilonInfo
   fn   := checkNoWsBeforeFn errorMsg
 }
@@ -1433,7 +1433,7 @@ position (see `withPosition`). This can be used to do whitespace sensitive synta
 a `by` block or `do` block, where all the lines have to line up.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkColEq (errorMsg : String := "checkColEq") : Parser where
+@[builtin_doc] def checkColEq (errorMsg : String := "checkColEq") : Parser where
   fn := checkColEqFn errorMsg
 
 def checkColGeFn (errorMsg : String) : ParserFn := fun c s =>
@@ -1452,7 +1452,7 @@ certain indentation scope. For example it is used in the lean grammar for `else
 that the `else` is not less indented than the `if` it matches with.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkColGe (errorMsg : String := "checkColGe") : Parser where
+@[builtin_doc] def checkColGe (errorMsg : String := "checkColGe") : Parser where
   fn := checkColGeFn errorMsg
 
 def checkColGtFn (errorMsg : String) : ParserFn := fun c s =>
@@ -1476,7 +1476,7 @@ Here, the `revert` tactic is followed by a list of `colGt ident`, because otherw
 interpret `exact` as an identifier and try to revert a variable named `exact`.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkColGt (errorMsg : String := "checkColGt") : Parser where
+@[builtin_doc] def checkColGt (errorMsg : String := "checkColGt") : Parser where
   fn := checkColGtFn errorMsg
 
 def checkLineEqFn (errorMsg : String) : ParserFn := fun c s =>
@@ -1494,7 +1494,7 @@ different lines. For example, `else if` is parsed using `lineEq` to ensure that
 are on the same line.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkLineEq (errorMsg : String := "checkLineEq") : Parser where
+@[builtin_doc] def checkLineEq (errorMsg : String := "checkLineEq") : Parser where
   fn := checkLineEqFn errorMsg
 
 /-- `withPosition(p)` runs `p` while setting the "saved position" to the current position.
@@ -1510,7 +1510,7 @@ The saved position is only available in the read-only state, which is why this i
 after the `withPosition(..)` block the saved position will be restored to its original value.
 
 This parser has the same arity as `p` - it just forwards the results of `p`. -/
-def withPosition : Parser → Parser := withFn fun f c s =>
+@[builtin_doc] def withPosition : Parser → Parser := withFn fun f c s =>
     adaptCacheableContextFn ({ · with savedPos? := s.pos }) f c s
 
 def withPositionAfterLinebreak : Parser → Parser := withFn fun f c s =>
@@ -1522,7 +1522,7 @@ parsers like `colGt` will have no effect. This is usually used by bracketing con
 `(...)` so that the user can locally override whitespace sensitivity.
 
 This parser has the same arity as `p` - it just forwards the results of `p`. -/
-def withoutPosition (p : Parser) : Parser :=
+@[builtin_doc] def withoutPosition (p : Parser) : Parser :=
   adaptCacheableContext ({ · with savedPos? := none }) p
 
 /-- `withForbidden tk p` runs `p` with `tk` as a "forbidden token". This means that if the token
@@ -1532,7 +1532,7 @@ stop there, making `tk` effectively a lowest-precedence operator. This is used f
 would be treated as an application.
 
 This parser has the same arity as `p` - it just forwards the results of `p`. -/
-def withForbidden (tk : Token) (p : Parser) : Parser :=
+@[builtin_doc] def withForbidden (tk : Token) (p : Parser) : Parser :=
   adaptCacheableContext ({ · with forbiddenTk? := tk }) p
 
 /-- `withoutForbidden(p)` runs `p` disabling the "forbidden token" (see `withForbidden`), if any.
@@ -1540,7 +1540,7 @@ This is usually used by bracketing constructs like `(...)` because there is no p
 inside these nested constructs.
 
 This parser has the same arity as `p` - it just forwards the results of `p`. -/
-def withoutForbidden (p : Parser) : Parser :=
+@[builtin_doc] def withoutForbidden (p : Parser) : Parser :=
   adaptCacheableContext ({ · with forbiddenTk? := none }) p
 
 def eoiFn : ParserFn := fun c s =>
@@ -1695,7 +1695,7 @@ def termParser (prec : Nat := 0) : Parser :=
 -- ==================
 
 /-- Fail if previous token is immediately followed by ':'. -/
-def checkNoImmediateColon : Parser := {
+@[builtin_doc] def checkNoImmediateColon : Parser := {
   fn := fun c s =>
     let prev := s.stxStack.back
     if checkTailNoWs prev then
@@ -1759,7 +1759,7 @@ def unicodeSymbol (sym asciiSym : String) : Parser :=
   Define parser for `$e` (if `anonymous == true`) and `$e:name`.
   `kind` is embedded in the antiquotation's kind, and checked at syntax `match` unless `isPseudoKind` is true.
   Antiquotations can be escaped as in `$$e`, which produces the syntax tree for `$e`. -/
-def mkAntiquot (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := false) : Parser :=
+@[builtin_doc] def mkAntiquot (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := false) : Parser :=
   let kind := kind ++ (if isPseudoKind then `pseudo else .anonymous) ++ `antiquot
   let nameP := node `antiquotName <| checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbol ":" >> nonReservedSymbol name
   -- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different
@@ -1784,7 +1784,7 @@ def withAntiquotFn (antiquotP p : ParserFn) (isCatAntiquot := false) : ParserFn
     p c s
 
 /-- Optimized version of `mkAntiquot ... <|> p`. -/
-def withAntiquot (antiquotP p : Parser) : Parser := {
+@[builtin_doc] def withAntiquot (antiquotP p : Parser) : Parser := {
   fn := withAntiquotFn antiquotP.fn p.fn
   info := orelseInfo antiquotP.info p.info
 }
@@ -1794,7 +1794,7 @@ def withoutInfo (p : Parser) : Parser := {
 }
 
 /-- Parse `$[p]suffix`, e.g. `$[p],*`. -/
-def mkAntiquotSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
+@[builtin_doc] def mkAntiquotSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
   let kind := kind ++ `antiquot_scope
   leadingNode kind maxPrec <| atomic <|
     setExpected [] "$" >>
@@ -1811,7 +1811,7 @@ private def withAntiquotSuffixSpliceFn (kind : SyntaxNodeKind) (suffix : ParserF
   s.mkNode (kind ++ `antiquot_suffix_splice) (s.stxStack.size - 2)
 
 /-- Parse `suffix` after an antiquotation, e.g. `$x,*`, and put both into a new node. -/
-def withAntiquotSuffixSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser where
+@[builtin_doc] def withAntiquotSuffixSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser where
   info := andthenInfo p.info suffix.info
   fn c s :=
     let s := p.fn c s
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 3b8ac2050afb..cd75143b581f 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -78,7 +78,7 @@ All modifiers are optional, and have to come in the listed order.
 `nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
 on the same line as the declaration. It is used for declarations nested inside other syntax,
 such as inductive constructors, structure projections, and `let rec` / `where` definitions. -/
-def declModifiers (inline : Bool) := leading_parser
+@[builtin_doc] def declModifiers (inline : Bool) := leading_parser
   optional docComment >>
   optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >>
   optional visibility >>
@@ -86,13 +86,16 @@ def declModifiers (inline : Bool) := leading_parser
   optional «unsafe» >>
   optional («partial» <|> «nonrec»)
 /-- `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names -/
-def declId           := leading_parser
+-- @[builtin_doc] -- FIXME: suppress the hover
+def declId := leading_parser
   ident >> optional (".{" >> sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}")
 /-- `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` -/
-def declSig          := leading_parser
+-- @[builtin_doc] -- FIXME: suppress the hover
+def declSig := leading_parser
   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.typeSpec
 /-- `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` -/
-def optDeclSig       := leading_parser
+-- @[builtin_doc] -- FIXME: suppress the hover
+def optDeclSig := leading_parser
   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
 def declValSimple    := leading_parser
   " :=" >> ppHardLineUnlessUngrouped >> termParser >> Termination.suffix >> optional Term.whereDecls
@@ -108,11 +111,11 @@ def whereStructInst  := leading_parser
 * a sequence of `| pat => expr` (a declaration by equations), shorthand for a `match`
 * `where` and then a sequence of `field := value` initializers, shorthand for a structure constructor
 -/
-def declVal          :=
+@[builtin_doc] def declVal :=
   -- Remark: we should not use `Term.whereDecls` at `declVal`
   -- because `Term.whereDecls` is defined using `Term.letRecDecl` which may contain attributes.
   -- Issue #753 shows an example that fails to be parsed when we used `Term.whereDecls`.
-  withAntiquot (mkAntiquot "declVal" `Lean.Parser.Command.declVal (isPseudoKind := true)) <|
+  withAntiquot (mkAntiquot "declVal" decl_name% (isPseudoKind := true)) <|
     declValSimple <|> declValEqns <|> whereStructInst
 def «abbrev»         := leading_parser
   "abbrev " >> declId >> ppIndent optDeclSig >> declVal
@@ -160,9 +163,10 @@ inductive List (α : Type u) where
 ```
 A list of elements of type `α` is either the empty list, `nil`,
 or an element `head : α` followed by a list `tail : List α`.
-For more information about [inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html).
+See [Inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html)
+for more information.
 -/
-def «inductive»      := leading_parser
+@[builtin_doc] def «inductive» := leading_parser
   "inductive " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> optional (symbol " :=" <|> " where") >>
   many ctor >> optional (ppDedent ppLine >> computedFields) >> optDeriving
 def classInductive   := leading_parser
@@ -442,7 +446,7 @@ def openSimple       := leading_parser
 def openScoped       := leading_parser
   " scoped" >> many1 (ppSpace >> checkColGt >> ident)
 /-- `openDecl` is the body of an `open` declaration (see `open`) -/
-def openDecl         :=
+@[builtin_doc] def openDecl :=
   withAntiquot (mkAntiquot "openDecl" `Lean.Parser.Command.openDecl (isPseudoKind := true)) <|
     openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped
 /-- Makes names from other namespaces visible without writing the namespace prefix.
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index c33c938e8253..63c4e360dba9 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -30,7 +30,7 @@ def doSeqBracketed := leading_parser
 do elements that take blocks. It can either have the form `"{" (doElem ";"?)* "}"` or
 `many1Indent (doElem ";"?)`, where `many1Indent` ensures that all the items are at
 the same or higher indentation level as the first line. -/
-def doSeq          :=
+@[builtin_doc] def doSeq :=
   withAntiquot (mkAntiquot "doSeq" decl_name% (isPseudoKind := true)) <|
     doSeqBracketed <|> doSeqIndent
 /-- `termBeforeDo` is defined as `withForbidden("do", term)`, which will parse a term but
diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean
index df5e1e807d1e..f3e64a578cd2 100644
--- a/src/Lean/Parser/Extra.lean
+++ b/src/Lean/Parser/Extra.lean
@@ -31,7 +31,7 @@ it to parse correctly. `ident?` will not work; one must write `(ident)?` instead
 This parser has arity 1: it produces a `nullKind` node containing either zero arguments
 (for the `none` case) or the list of arguments produced by `p`.
 (In particular, if `p` has arity 0 then the two cases are not differentiated!) -/
-@[run_builtin_parser_attribute_hooks] def optional (p : Parser) : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def optional (p : Parser) : Parser :=
   optionalNoAntiquot (withAntiquotSpliceAndSuffix `optional p (symbol "?"))
 
 /-- The parser `many(p)`, or `p*`, repeats `p` until it fails, and returns the list of results.
@@ -41,7 +41,7 @@ automatically replaced by `group(p)` to ensure that it produces exactly 1 value.
 
 This parser has arity 1: it produces a `nullKind` node containing one argument for each
 invocation of `p` (or `group(p)`). -/
-@[run_builtin_parser_attribute_hooks] def many (p : Parser) : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def many (p : Parser) : Parser :=
   manyNoAntiquot (withAntiquotSpliceAndSuffix `many p (symbol "*"))
 
 /-- The parser `many1(p)`, or `p+`, repeats `p` until it fails, and returns the list of results.
@@ -56,7 +56,7 @@ automatically replaced by `group(p)` to ensure that it produces exactly 1 value.
 
 This parser has arity 1: it produces a `nullKind` node containing one argument for each
 invocation of `p` (or `group(p)`). -/
-@[run_builtin_parser_attribute_hooks] def many1 (p : Parser) : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def many1 (p : Parser) : Parser :=
   many1NoAntiquot (withAntiquotSpliceAndSuffix `many p (symbol "*"))
 
 /-- The parser `ident` parses a single identifier, possibly with namespaces, such as `foo` or
@@ -70,18 +70,18 @@ using disallowed characters in identifiers such as `«foo.bar».baz` or `«hello
 
 This parser has arity 1: it produces a `Syntax.ident` node containing the parsed identifier.
 You can use `TSyntax.getId` to extract the name from the resulting syntax object. -/
-@[run_builtin_parser_attribute_hooks] def ident : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def ident : Parser :=
   withAntiquot (mkAntiquot "ident" identKind) identNoAntiquot
 
 -- `optional (checkNoWsBefore >> "." >> checkNoWsBefore >> ident)`
 -- can never fully succeed but ensures that the identifier
 -- produces a partial syntax that contains the dot.
 -- The partial syntax is sometimes useful for dot-auto-completion.
-@[run_builtin_parser_attribute_hooks] def identWithPartialTrailingDot :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def identWithPartialTrailingDot :=
   ident >> optional (checkNoWsBefore >> "." >> checkNoWsBefore >> ident)
 
 -- `ident` and `rawIdent` produce the same syntax tree, so we reuse the antiquotation kind name
-@[run_builtin_parser_attribute_hooks] def rawIdent : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def rawIdent : Parser :=
   withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot
 
 /-- The parser `hygieneInfo` parses no text, but captures the current macro scope information
@@ -96,7 +96,7 @@ for more information about macro hygiene.
 
 This parser has arity 1: it produces a `Syntax.ident` node containing the parsed identifier.
 You can use `TSyntax.getHygieneInfo` to extract the name from the resulting syntax object. -/
-@[run_builtin_parser_attribute_hooks] def hygieneInfo : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def hygieneInfo : Parser :=
   withAntiquot (mkAntiquot "hygieneInfo" hygieneInfoKind (anonymous := false)) hygieneInfoNoAntiquot
 
 /-- The parser `num` parses a numeric literal in several bases:
@@ -109,7 +109,7 @@ You can use `TSyntax.getHygieneInfo` to extract the name from the resulting synt
 This parser has arity 1: it produces a `numLitKind` node containing an atom with the text of the
 literal.
 You can use `TSyntax.getNat` to extract the number from the resulting syntax object. -/
-@[run_builtin_parser_attribute_hooks] def numLit : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def numLit : Parser :=
   withAntiquot (mkAntiquot "num" numLitKind) numLitNoAntiquot
 
 /-- The parser `scientific` parses a scientific-notation literal, such as `1.3e-24`.
@@ -117,7 +117,7 @@ You can use `TSyntax.getNat` to extract the number from the resulting syntax obj
 This parser has arity 1: it produces a `scientificLitKind` node containing an atom with the text
 of the literal.
 You can use `TSyntax.getScientific` to extract the parts from the resulting syntax object. -/
-@[run_builtin_parser_attribute_hooks] def scientificLit : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def scientificLit : Parser :=
   withAntiquot (mkAntiquot "scientific" scientificLitKind) scientificLitNoAntiquot
 
 /-- The parser `str` parses a string literal, such as `"foo"` or `"\r\n"`. Strings can contain
@@ -127,7 +127,7 @@ Newlines in a string are interpreted literally.
 This parser has arity 1: it produces a `strLitKind` node containing an atom with the raw
 literal (including the quote marks and without interpreting the escapes).
 You can use `TSyntax.getString` to decode the string from the resulting syntax object. -/
-@[run_builtin_parser_attribute_hooks] def strLit : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def strLit : Parser :=
   withAntiquot (mkAntiquot "str" strLitKind) strLitNoAntiquot
 
 /-- The parser `char` parses a character literal, such as `'a'` or `'\n'`. Character literals can
@@ -138,7 +138,7 @@ like `∈`, but must evaluate to a single unicode codepoint, so `'♥'` is allow
 This parser has arity 1: it produces a `charLitKind` node containing an atom with the raw
 literal (including the quote marks and without interpreting the escapes).
 You can use `TSyntax.getChar` to decode the string from the resulting syntax object. -/
-@[run_builtin_parser_attribute_hooks] def charLit : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def charLit : Parser :=
   withAntiquot (mkAntiquot "char" charLitKind) charLitNoAntiquot
 
 /-- The parser `name` parses a name literal like `` `foo``. The syntax is the same as for identifiers
@@ -147,7 +147,7 @@ You can use `TSyntax.getChar` to decode the string from the resulting syntax obj
 This parser has arity 1: it produces a `nameLitKind` node containing the raw literal
 (including the backquote).
 You can use `TSyntax.getName` to extract the name from the resulting syntax object. -/
-@[run_builtin_parser_attribute_hooks] def nameLit : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] def nameLit : Parser :=
   withAntiquot (mkAntiquot "name" nameLitKind) nameLitNoAntiquot
 
 /-- The parser `group(p)` parses the same thing as `p`, but it wraps the results in a `groupKind`
@@ -156,7 +156,7 @@ node.
 This parser always has arity 1, even if `p` does not. Parsers like `p*` are automatically
 rewritten to `group(p)*` if `p` does not have arity 1, so that the results from separate invocations
 of `p` can be differentiated. -/
-@[run_builtin_parser_attribute_hooks, inline] def group (p : Parser) : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc, inline] def group (p : Parser) : Parser :=
   node groupKind p
 
 /-- The parser `many1Indent(p)` is equivalent to `withPosition((colGe p)+)`. This has the effect of
@@ -165,7 +165,7 @@ the same or more than the first parse.
 
 This parser has arity 1, and returns a list of the results from `p`.
 `p` is "auto-grouped" if it is not arity 1. -/
-@[run_builtin_parser_attribute_hooks, inline] def many1Indent (p : Parser) : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc, inline] def many1Indent (p : Parser) : Parser :=
   withPosition $ many1 (checkColGe "irrelevant" >> p)
 
 /-- The parser `manyIndent(p)` is equivalent to `withPosition((colGe p)*)`. This has the effect of
@@ -174,14 +174,14 @@ the same or more than the first parse.
 
 This parser has arity 1, and returns a list of the results from `p`.
 `p` is "auto-grouped" if it is not arity 1. -/
-@[run_builtin_parser_attribute_hooks, inline] def manyIndent (p : Parser) : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc, inline] def manyIndent (p : Parser) : Parser :=
   withPosition $ many (checkColGe "irrelevant" >> p)
 
-@[inline] def sepByIndent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
+@[builtin_doc, inline] def sepByIndent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
   let p := withAntiquotSpliceAndSuffix `sepBy p (symbol "*")
   withPosition $ sepBy (checkColGe "irrelevant" >> p) sep (psep <|> checkColEq "irrelevant" >> checkLinebreakBefore >> pushNone) allowTrailingSep
 
-@[inline] def sepBy1Indent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
+@[builtin_doc, inline] def sepBy1Indent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
   let p := withAntiquotSpliceAndSuffix `sepBy p (symbol "*")
   withPosition $ sepBy1 (checkColGe "irrelevant" >> p) sep (psep <|> checkColEq "irrelevant" >> checkLinebreakBefore >> pushNone) allowTrailingSep
 
@@ -205,32 +205,33 @@ def sepByIndent.formatter (p : Formatter) (_sep : String) (pSep : Formatter) : F
 
 attribute [run_builtin_parser_attribute_hooks] sepByIndent sepBy1Indent
 
-@[run_builtin_parser_attribute_hooks] abbrev notSymbol (s : String) : Parser :=
+@[run_builtin_parser_attribute_hooks, builtin_doc] 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
+@[run_builtin_parser_attribute_hooks, builtin_doc, inline]
+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
+@[builtin_doc, inline] def ppHardSpace : Parser := skip
 /-- No-op parser that advises the pretty printer to emit a space/soft line break. -/
-@[inline] def ppSpace : Parser := skip
+@[builtin_doc, inline] def ppSpace : Parser := skip
 /-- No-op parser that advises the pretty printer to emit a hard line break. -/
-@[inline] def ppLine : Parser := skip
+@[builtin_doc, inline] def ppLine : Parser := skip
 /-- No-op parser combinator that advises the pretty printer to emit a `Format.fill` node. -/
-@[inline] def ppRealFill : Parser → Parser := id
+@[builtin_doc, inline] def ppRealFill : Parser → Parser := id
 /-- No-op parser combinator that advises the pretty printer to emit a `Format.group` node. -/
-@[inline] def ppRealGroup : Parser → Parser := id
+@[builtin_doc, inline] def ppRealGroup : Parser → Parser := id
 /-- No-op parser combinator that advises the pretty printer to indent the given syntax without grouping it. -/
-@[inline] def ppIndent : Parser → Parser := id
+@[builtin_doc, inline] def ppIndent : Parser → Parser := id
 /--
   No-op parser combinator that advises the pretty printer to group and indent the given syntax.
   By default, only syntax categories are grouped. -/
-@[inline] def ppGroup (p : Parser) : Parser := ppRealFill (ppIndent p)
+@[builtin_doc, inline] def ppGroup (p : Parser) : Parser := ppRealFill (ppIndent p)
 /--
   No-op parser combinator that advises the pretty printer to dedent the given syntax.
   Dedenting can in particular be used to counteract automatic indentation. -/
-@[inline] def ppDedent : Parser → Parser := id
+@[builtin_doc, inline] def ppDedent : Parser → Parser := id
 
 /--
   No-op parser combinator that allows the pretty printer to omit the group and
@@ -242,19 +243,19 @@ attribute [run_builtin_parser_attribute_hooks] sepByIndent sepBy1Indent
     trivial
   ```
 -/
-@[inline] def ppAllowUngrouped : Parser := skip
+@[builtin_doc, inline] def ppAllowUngrouped : Parser := skip
 
 /--
   No-op parser combinator that advises the pretty printer to dedent the given syntax,
   if it was grouped by the category parser.
   Dedenting can in particular be used to counteract automatic indentation. -/
-@[inline] def ppDedentIfGrouped : Parser → Parser := id
+@[builtin_doc, inline] def ppDedentIfGrouped : Parser → Parser := id
 
 /--
   No-op parser combinator that prints a line break.
   The line break is soft if the combinator is followed
   by an ungrouped parser (see ppAllowUngrouped), otherwise hard. -/
-@[inline] def ppHardLineUnlessUngrouped : Parser := skip
+@[builtin_doc, inline] def ppHardLineUnlessUngrouped : Parser := skip
 
 end Parser
 
diff --git a/src/Lean/Parser/StrInterpolation.lean b/src/Lean/Parser/StrInterpolation.lean
index 1aeecf7ab10d..998da4a0d3b3 100644
--- a/src/Lean/Parser/StrInterpolation.lean
+++ b/src/Lean/Parser/StrInterpolation.lean
@@ -68,7 +68,7 @@ This parser has arity 1, and returns a `interpolatedStrKind` with an odd number
 alternating between chunks of literal text and results from `p`. The literal chunks contain
 uninterpreted substrings of the input. For example, `"foo\n{2 + 2}"` would have three arguments:
 an atom `"foo\n{`, the parsed `2 + 2` term, and then the atom `}"`. -/
-def interpolatedStr (p : Parser) : Parser :=
+@[builtin_doc] def interpolatedStr (p : Parser) : Parser :=
   withAntiquot (mkAntiquot "interpolatedStr" interpolatedStrKind) $ interpolatedStrNoAntiquot p
 
 end Lean.Parser
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 6ffe3e4be7e9..065e276882c2 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -24,6 +24,7 @@ a regular comment (that is, as whitespace); it is parsed and forms part of the s
 
 A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
 example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. -/
+-- @[builtin_doc] -- FIXME: suppress the hover
 def docComment := leading_parser
   ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine
 end Command
@@ -49,7 +50,7 @@ example := by
   skip
 ```
 is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
-@[run_builtin_parser_attribute_hooks]
+@[run_builtin_parser_attribute_hooks, builtin_doc]
 def sepByIndentSemicolon (p : Parser) : Parser :=
   sepByIndent p "; " (allowTrailingSep := true)
 
@@ -62,7 +63,7 @@ example := by
   skip
 ```
 is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
-@[run_builtin_parser_attribute_hooks]
+@[run_builtin_parser_attribute_hooks, builtin_doc]
 def sepBy1IndentSemicolon (p : Parser) : Parser :=
   sepBy1Indent p "; " (allowTrailingSep := true)
 
@@ -70,22 +71,22 @@ builtin_initialize
   register_parser_alias sepByIndentSemicolon
   register_parser_alias sepBy1IndentSemicolon
 
-def tacticSeq1Indented : Parser := leading_parser
+@[builtin_doc] def tacticSeq1Indented : Parser := leading_parser
   sepBy1IndentSemicolon tacticParser
 /-- The syntax `{ tacs }` is an alternative syntax for `· tacs`.
 It runs the tactics in sequence, and fails if the goal is not solved. -/
-def tacticSeqBracketed : Parser := leading_parser
+@[builtin_doc] def tacticSeqBracketed : Parser := leading_parser
   "{" >> sepByIndentSemicolon tacticParser >> ppDedent (ppLine >> "}")
 
 /-- A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
 Delimiter-free indentation is determined by the *first* tactic of the sequence. -/
-def tacticSeq := leading_parser
+@[builtin_doc] def tacticSeq := leading_parser
   tacticSeqBracketed <|> tacticSeq1Indented
 
 /-- Same as [`tacticSeq`] but requires delimiter-free tactic sequence to have strict indentation.
 The strict indentation requirement only apply to *nested* `by`s, as top-level `by`s do not have a
 position set. -/
-def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
+@[builtin_doc] def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
   tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented)
 
 /- Raw sequence for quotation and grouping -/
@@ -204,7 +205,7 @@ def fromTerm   := leading_parser
 def showRhs := fromTerm <|> byTactic'
 /-- A `sufficesDecl` represents everything that comes after the `suffices` keyword:
 an optional `x :`, then a term `ty`, then `from val` or `by tac`. -/
-def sufficesDecl := leading_parser
+@[builtin_doc] def sufficesDecl := leading_parser
   (atomic (group (binderIdent >> " : ")) <|> hygieneInfo) >> termParser >> ppSpace >> showRhs
 @[builtin_term_parser] def «suffices» := leading_parser:leadPrec
   withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
@@ -270,7 +271,7 @@ open Lean.PrettyPrinter Parenthesizer Syntax.MonadTraverser in
 Explicit binder, like `(x y : A)` or `(x y)`.
 Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
 -/
-def explicitBinder (requireType := false) := leading_parser ppGroup <|
+@[builtin_doc] def explicitBinder (requireType := false) := leading_parser ppGroup <|
   "(" >> withoutPosition (many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault)) >> ")"
 /--
 Implicit binder, like `{x y : A}` or `{x y}`.
@@ -281,7 +282,7 @@ by unification.
 
 In `@` explicit mode, implicit binders behave like explicit binders.
 -/
-def implicitBinder (requireType := false) := leading_parser ppGroup <|
+@[builtin_doc] def implicitBinder (requireType := false) := leading_parser ppGroup <|
   "{" >> withoutPosition (many1 binderIdent >> binderType requireType) >> "}"
 def strictImplicitLeftBracket := atomic (group (symbol "{" >> "{")) <|> "⦃"
 def strictImplicitRightBracket := atomic (group (symbol "}" >> "}")) <|> "⦄"
@@ -298,7 +299,7 @@ and `h hs` has type `p y`.
 In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
 with `?m` a fresh metavariable.
 -/
-def strictImplicitBinder (requireType := false) := leading_parser ppGroup <|
+@[builtin_doc] def strictImplicitBinder (requireType := false) := leading_parser ppGroup <|
   strictImplicitLeftBracket >> many1 binderIdent >>
   binderType requireType >> strictImplicitRightBracket
 /--
@@ -308,7 +309,7 @@ and solved for by typeclass inference for the specified class `C`.
 In `@` explicit mode, if `_` is used for an an instance-implicit parameter, then it is still solved for by typeclass inference;
 use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
 -/
-def instBinder := leading_parser ppGroup <|
+@[builtin_doc] def instBinder := leading_parser ppGroup <|
   "[" >> withoutPosition (optIdent >> termParser) >> "]"
 /-- A `bracketedBinder` matches any kind of binder group that uses some kind of brackets:
 * An explicit binder like `(x y : A)`
@@ -316,7 +317,7 @@ def instBinder := leading_parser ppGroup <|
 * A strict implicit binder, `⦃y z : A⦄` or its ASCII alternative `{{y z : A}}`
 * An instance binder `[A]` or `[x : A]` (multiple variables are not allowed here)
 -/
-def bracketedBinder (requireType := false) :=
+@[builtin_doc] def bracketedBinder (requireType := false) :=
   withAntiquot (mkAntiquot "bracketedBinder" decl_name% (isPseudoKind := true)) <|
     explicitBinder requireType <|> strictImplicitBinder requireType <|>
     implicitBinder requireType <|> instBinder
@@ -364,7 +365,7 @@ def matchAlts (rhsParser : Parser := termParser) : Parser :=
 
 /-- `matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
 `match h1 : e1, e2, h3 : e3 with ...`. -/
-def matchDiscr := leading_parser
+@[builtin_doc] def matchDiscr := leading_parser
   optional (atomic (ident >> " : ")) >> termParser
 
 def trueVal  := leading_parser nonReservedSymbol "true"
@@ -495,7 +496,7 @@ def letEqnsDecl := leading_parser (withAnonymousAntiquot := false)
 `let pat := e` (where `pat` is an arbitrary term) or `let f | pat1 => e1 | pat2 => e2 ...`
 (a pattern matching declaration), except for the `let` keyword itself.
 `let rec` declarations are not handled here. -/
-def letDecl     := leading_parser (withAnonymousAntiquot := false)
+@[builtin_doc] def letDecl := leading_parser (withAnonymousAntiquot := false)
   -- Remark: we disable anonymous antiquotations here to make sure
   -- anonymous antiquotations (e.g., `$x`) are not `letDecl`
   notFollowedBy (nonReservedSymbol "rec") "rec" >>
@@ -551,7 +552,7 @@ def haveEqnsDecl := leading_parser (withAnonymousAntiquot := false)
 /-- `haveDecl` matches the body of a have declaration: `have := e`, `have f x1 x2 := e`,
 `have pat := e` (where `pat` is an arbitrary term) or `have f | pat1 => e1 | pat2 => e2 ...`
 (a pattern matching declaration), except for the `have` keyword itself. -/
-def haveDecl     := leading_parser (withAnonymousAntiquot := false)
+@[builtin_doc] def haveDecl := leading_parser (withAnonymousAntiquot := false)
   haveIdDecl <|> (ppSpace >> letPatDecl) <|> haveEqnsDecl
 @[builtin_term_parser] def «have» := leading_parser:leadPrec
   withPosition ("have" >> haveDecl) >> optSemicolon termParser
@@ -565,7 +566,7 @@ def haveDecl     := leading_parser (withAnonymousAntiquot := false)
 def «scoped» := leading_parser "scoped "
 def «local»  := leading_parser "local "
 /-- `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. -/
-def attrKind := leading_parser optional («scoped» <|> «local»)
+@[builtin_doc] def attrKind := leading_parser optional («scoped» <|> «local»)
 def attrInstance     := ppGroup $ leading_parser attrKind >> attrParser
 
 def attributes       := leading_parser
@@ -596,12 +597,12 @@ termination_by b c => a - b
 If omitted, a termination argument will be inferred. If written as `termination_by?`,
 the inferrred termination argument will be suggested.
 -/
-def terminationBy := leading_parser
+@[builtin_doc] def terminationBy := leading_parser
   "termination_by " >>
   optional (atomic (many (ppSpace >> Term.binderIdent) >> " => ")) >>
   termParser
 
-@[inherit_doc terminationBy]
+@[inherit_doc terminationBy, builtin_doc]
 def terminationBy? := leading_parser
   "termination_by?"
 
@@ -611,13 +612,13 @@ decreases at each recursive call.
 
 By default, the tactic `decreasing_tactic` is used.
 -/
-def decreasingBy := leading_parser
+@[builtin_doc] def decreasingBy := leading_parser
   ppDedent ppLine >> "decreasing_by " >> Tactic.tacticSeqIndentGt
 
 /--
 Termination hints are `termination_by` and `decreasing_by`, in that order.
 -/
-def suffix := leading_parser
+@[builtin_doc] def suffix := leading_parser
   optional (ppDedent ppLine >> (terminationBy? <|> terminationBy)) >> optional decreasingBy
 
 end Termination
@@ -625,9 +626,10 @@ namespace Term
 
 /-- `letRecDecl` matches the body of a let-rec declaration: a doc comment, attributes, and then
 a let declaration without the `let` keyword, such as `/-- foo -/ @[simp] bar := 1`. -/
-def letRecDecl       := leading_parser
+@[builtin_doc] def letRecDecl := leading_parser
   optional Command.docComment >> optional «attributes» >> letDecl >> Termination.suffix
 /-- `letRecDecls` matches `letRecDecl,+`, a comma-separated list of let-rec declarations (see `letRecDecl`). -/
+-- @[builtin_doc] -- FIXME: suppress the hover
 def letRecDecls      := leading_parser
   sepBy1 letRecDecl ", "
 @[builtin_term_parser]
diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean
index 30f4a316636f..22d5707c72de 100644
--- a/src/Lean/Parser/Types.lean
+++ b/src/Lean/Parser/Types.lean
@@ -7,6 +7,7 @@ prelude
 import Lean.Data.Trie
 import Lean.Syntax
 import Lean.Message
+import Lean.DocString
 
 namespace Lean.Parser
 
@@ -428,7 +429,7 @@ def withCacheFn (parserName : Name) (p : ParserFn) : ParserFn := fun c s => Id.r
     panic! s!"withCacheFn: unexpected stack growth {s.stxStack.raw}"
   { s with cache.parserCache := s.cache.parserCache.insert key ⟨s.stxStack.back, s.lhsPrec, s.pos, s.errorMsg⟩ }
 
-@[inherit_doc withCacheFn]
+@[inherit_doc withCacheFn, builtin_doc]
 def withCache (parserName : Name) : Parser → Parser := withFn (withCacheFn parserName)
 
 def ParserFn.run (p : ParserFn) (ictx : InputContext) (pmctx : ParserModuleContext) (tokens : TokenTable) (s : ParserState) : ParserState :=

From edc6182848e18da220ec07c3ef8d62851eb4870b Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sat, 20 Apr 2024 12:57:54 -0400
Subject: [PATCH 2/3] fix test

---
 tests/lean/interactive/hoverException.lean.expected.out | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tests/lean/interactive/hoverException.lean.expected.out b/tests/lean/interactive/hoverException.lean.expected.out
index af093fa3a839..02bb79ad4795 100644
--- a/tests/lean/interactive/hoverException.lean.expected.out
+++ b/tests/lean/interactive/hoverException.lean.expected.out
@@ -1,3 +1,8 @@
 {"textDocument": {"uri": "file:///hoverException.lean"},
  "position": {"line": 2, "character": 14}}
-null
+{"range":
+ {"start": {"line": 2, "character": 7}, "end": {"line": 2, "character": 18}},
+ "contents":
+ {"value":
+  "Explicit binder, like `(x y : A)` or `(x y)`.\nDefault values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.\n",
+  "kind": "markdown"}}

From 612254dfc3af417056afce11b414c87e00d081f4 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Fri, 13 Sep 2024 11:10:01 +0400
Subject: [PATCH 3/3] allow inherit_doc and builtin_doc together

---
 src/Lean/Elab/InheritDoc.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/InheritDoc.lean b/src/Lean/Elab/InheritDoc.lean
index 377f9f595217..ecc5f316517e 100644
--- a/src/Lean/Elab/InheritDoc.lean
+++ b/src/Lean/Elab/InheritDoc.lean
@@ -21,7 +21,7 @@ builtin_initialize
         let some id := id?
           | throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
         let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
-        if (← findSimpleDocString? (← getEnv) decl).isSome then
+        if (← findSimpleDocString? (← getEnv) decl (includeBuiltin := false)).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
         let some doc ← findSimpleDocString? (← getEnv) declName
           | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"