From ac92134066efc17d628c7f661106922bcb89205a Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 15 Apr 2024 16:12:00 -0400
Subject: [PATCH] feat: @[builtin_doc] attribute (part 1)

---
 src/Lean/BuiltinDocAttr.lean   | 27 +++++++++++++++++++++++++++
 src/Lean/Elab/Util.lean        |  5 +----
 src/Lean/Parser/Extension.lean |  8 ++------
 3 files changed, 30 insertions(+), 10 deletions(-)
 create mode 100644 src/Lean/BuiltinDocAttr.lean

diff --git a/src/Lean/BuiltinDocAttr.lean b/src/Lean/BuiltinDocAttr.lean
new file mode 100644
index 000000000000..93f55edc3e10
--- /dev/null
+++ b/src/Lean/BuiltinDocAttr.lean
@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2024 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+prelude
+import Lean.Compiler.InitAttr
+import Lean.DocString
+
+namespace Lean
+
+def declareBuiltinDocStringAndRanges (declName : Name) : AttrM Unit := do
+  if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
+    declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
+  if let some declRanges ← findDeclarationRanges? declName then
+    declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name  := `builtin_doc
+    descr := "make the docs and location of this declaration available as a builtin"
+    add   := fun decl stx _ => do
+      Attribute.Builtin.ensureNoArgs stx
+      declareBuiltinDocStringAndRanges decl
+  }
+
+end Lean
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 53235977b2f6..f453d1d14c24 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -114,10 +114,7 @@ unsafe def mkElabAttribute (γ) (attrBuiltinName attrName : Name) (parserNamespa
       return kind
     onAdded       := fun builtin declName => do
       if builtin then
-        if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
-          declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
-        if let some declRanges ← findDeclarationRanges? declName then
-          declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
+        declareBuiltinDocStringAndRanges declName
   } attrDeclName
 
 unsafe def mkMacroAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute Macro) :=
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 8978a2153a4e..562900d894fd 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -5,9 +5,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Parser.Basic
-import Lean.Compiler.InitAttr
 import Lean.ScopedEnvExtension
-import Lean.DocString
+import Lean.BuiltinDocAttr
 
 /-! Extensible parsing via attributes -/
 
@@ -488,10 +487,7 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
   | Expr.const `Lean.Parser.Parser _ =>
     declareLeadingBuiltinParser catName declName prio
   | _ => throwError "unexpected parser type at '{declName}' (`Parser` or `TrailingParser` expected)"
-  if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
-    declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
-  if let some declRanges ← findDeclarationRanges? declName then
-    declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
+  declareBuiltinDocStringAndRanges declName
   runParserAttributeHooks catName declName (builtin := true)
 
 /--