fix: built-in parser attributes link to the wrong place (#3916)
Go-to-def on `@[builtin_term_parser]` should go to the line
```lean
builtin_initialize registerBuiltinParserAttribute `builtin_term_parser ``Category.term
```
not
```lean
/-- `term` is the builtin syntax category for terms. ... -/
def term : Category := {}
```
This commit is contained in:
parent
faa4d16dc1
commit
df1e6ba7fe
1 changed files with 2 additions and 2 deletions
|
|
@ -498,13 +498,13 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
|
|||
The parsing tables for builtin parsers are "stored" in the extracted source code.
|
||||
-/
|
||||
def registerBuiltinParserAttribute (attrName declName : Name)
|
||||
(behavior := LeadingIdentBehavior.default) : IO Unit := do
|
||||
(behavior := LeadingIdentBehavior.default) (ref : Name := by exact decl_name%) : IO Unit := do
|
||||
let .str ``Lean.Parser.Category s := declName
|
||||
| throw (IO.userError "`declName` should be in Lean.Parser.Category")
|
||||
let catName := Name.mkSimple s
|
||||
addBuiltinParserCategory catName declName behavior
|
||||
registerBuiltinAttribute {
|
||||
ref := declName
|
||||
ref := ref
|
||||
name := attrName
|
||||
descr := "Builtin parser"
|
||||
add := fun declName stx kind => liftM $ BuiltinParserAttribute.add attrName catName declName stx kind
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue