From df1e6ba7fefdce90f8c655cb2c1bf5ea8640d1a5 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 18 Apr 2024 04:28:16 -0400 Subject: [PATCH] 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 := {} ``` --- src/Lean/Parser/Extension.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index db2d2e47c9..8978a2153a 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -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