chore: use Category declarations for builtin cats too (#1400)

src/Init/Notation.lean

@@ -22,6 +22,8 @@ def term : Category := {}
 def tactic : Category := {}
 /-- The syntax category for elements that can appear in the `do` notation. -/
 def doElem : Category := {}
+/-- The level syntax category. -/
+def level : Category := {}
 /-- The attribute syntax category. Declarations can be annotated with attributes using the `@[...]` notation. -/
 def attr : Category := {}
 /-- The syntax syntax category. This is the syntax category used to define syntax itself. -/

src/Lean/Parser/Attr.lean

@@ -9,11 +9,11 @@ import Lean.Parser.Extra
 namespace Lean.Parser
 
 builtin_initialize
-  registerBuiltinParserAttribute `builtinPrioParser `prio LeadingIdentBehavior.both
+  registerBuiltinParserAttribute `builtinPrioParser ``Category.prio .both
   registerBuiltinDynamicParserAttribute `prioParser `prio
 
 builtin_initialize
-  registerBuiltinParserAttribute `builtinAttrParser `attr LeadingIdentBehavior.symbol
+  registerBuiltinParserAttribute `builtinAttrParser ``Category.attr .symbol
   registerBuiltinDynamicParserAttribute `attrParser `attr
 
 @[inline] def priorityParser (rbp : Nat := 0) : Parser :=

src/Lean/Parser/Basic.lean

@@ -1614,10 +1614,9 @@ inductive LeadingIdentBehavior where
 structure ParserCategory where
   /-- The name of a declaration which will be used as the target of
   go-to-definition queries and from which doc strings will be extracted.
-  This is usually a dummy declaration of type `Lean.Parser.Category`
-  created by `declare_syntax_cat`, but for builtin categories this will
-  be the `builtin_initialize` command containing the call to
-  `registerBuiltinParserAttribute`. -/
+  This is a dummy declaration of type `Lean.Parser.Category`
+  created by `declare_syntax_cat`, but for builtin categories the declaration
+  is made manually and passed to `registerBuiltinParserAttribute`. -/
   declName : Name
   /-- The list of syntax nodes that can parse into this category.
   This can be used to list all syntaxes in the category. -/

src/Lean/Parser/Do.lean

@@ -8,7 +8,7 @@ import Lean.Parser.Term
 namespace Lean
 namespace Parser
 
-builtin_initialize registerBuiltinParserAttribute `builtinDoElemParser `doElem
+builtin_initialize registerBuiltinParserAttribute `builtinDoElemParser ``Category.doElem
 builtin_initialize registerBuiltinDynamicParserAttribute `doElemParser `doElem
 
 @[inline] def doElemParser (rbp : Nat := 0) : Parser :=

src/Lean/Parser/Extension.lean

@@ -509,11 +509,14 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
 /--
 The parsing tables for builtin parsers are "stored" in the extracted source code.
 -/
-def registerBuiltinParserAttribute (attrName : Name) (catName : Name)
-    (behavior := LeadingIdentBehavior.default) (ref : Name := by exact decl_name%) : IO Unit := do
-  addBuiltinParserCategory catName ref behavior
+def registerBuiltinParserAttribute (attrName declName : Name)
+    (behavior := LeadingIdentBehavior.default) : 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             := ref
+    ref             := declName
     name            := attrName
     descr           := "Builtin parser"
     add             := fun declName stx kind => liftM $ BuiltinParserAttribute.add attrName catName declName stx kind
@@ -566,12 +569,12 @@ def registerParserCategory (env : Environment) (attrName catName : Name)
 
 -- declare `termParser` here since it is used everywhere via antiquotations
 
-builtin_initialize registerBuiltinParserAttribute `builtinTermParser `term
+builtin_initialize registerBuiltinParserAttribute `builtinTermParser ``Category.term
 
 builtin_initialize registerBuiltinDynamicParserAttribute `termParser `term
 
 -- declare `commandParser` to break cyclic dependency
-builtin_initialize registerBuiltinParserAttribute `builtinCommandParser `command
+builtin_initialize registerBuiltinParserAttribute `builtinCommandParser ``Category.command
 
 builtin_initialize registerBuiltinDynamicParserAttribute `commandParser `command
 

src/Lean/Parser/Level.lean

@@ -9,7 +9,7 @@ namespace Lean
 namespace Parser
 
 builtin_initialize
-  registerBuiltinParserAttribute `builtinLevelParser `level
+  registerBuiltinParserAttribute `builtinLevelParser ``Category.level
 
 @[inline] def levelParser (rbp : Nat := 0) : Parser :=
   categoryParser `level rbp

src/Lean/Parser/Syntax.lean

@@ -10,11 +10,11 @@ namespace Lean
 namespace Parser
 
 builtin_initialize
-  registerBuiltinParserAttribute `builtinSyntaxParser `stx LeadingIdentBehavior.both
+  registerBuiltinParserAttribute `builtinSyntaxParser ``Category.stx .both
   registerBuiltinDynamicParserAttribute `stxParser `stx
 
 builtin_initialize
-  registerBuiltinParserAttribute `builtinPrecParser `prec LeadingIdentBehavior.both
+  registerBuiltinParserAttribute `builtinPrecParser ``Category.prec .both
   registerBuiltinDynamicParserAttribute `precParser `prec
 
 @[inline] def precedenceParser (rbp : Nat := 0) : Parser :=

src/Lean/Parser/Term.lean

@@ -16,11 +16,11 @@ def commentBody : Parser :=
 @[combinatorParenthesizer Lean.Parser.Command.commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
 @[combinatorFormatter Lean.Parser.Command.commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
 
-def docComment       := leading_parser ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine
+def docComment := leading_parser ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine
 end Command
 
 builtin_initialize
-  registerBuiltinParserAttribute `builtinTacticParser `tactic LeadingIdentBehavior.both
+  registerBuiltinParserAttribute `builtinTacticParser ``Category.tactic .both
   registerBuiltinDynamicParserAttribute `tacticParser `tactic
 
 @[inline] def tacticParser (rbp : Nat := 0) : Parser :=