diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index 3e1a0106e8..d9c5f2cc4b 100644
--- a/src/Lean/Data/Position.lean
+++ b/src/Lean/Data/Position.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Data.Format
+import Lean.ToExpr
 
 namespace Lean
 
@@ -21,6 +22,11 @@ instance : ToFormat Position :=
 
 instance : ToString Position :=
   ⟨fun ⟨l, c⟩ => "⟨" ++ toString l ++ ", " ++ toString c ++ "⟩"⟩
+
+instance : ToExpr Position where
+  toExpr p   := mkAppN (mkConst ``Position.mk) #[toExpr p.line, toExpr p.column]
+  toTypeExpr := mkConst ``Position
+
 end Position
 
 structure FileMap where
diff --git a/src/Lean/DeclarationRange.lean b/src/Lean/DeclarationRange.lean
index 4d8e4e5e4c..19ec43adef 100644
--- a/src/Lean/DeclarationRange.lean
+++ b/src/Lean/DeclarationRange.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.MonadEnv
 import Lean.AuxRecursor
+import Lean.ToExpr
 
 namespace Lean
 
@@ -20,20 +21,34 @@ structure DeclarationRange where
   endCharUtf16 : Nat
   deriving Inhabited, DecidableEq, Repr
 
+instance : ToExpr DeclarationRange where
+  toExpr r   := mkAppN (mkConst ``DeclarationRange.mk) #[toExpr r.pos, toExpr r.charUtf16, toExpr r.endPos, toExpr r.endCharUtf16]
+  toTypeExpr := mkConst ``DeclarationRange
+
 structure DeclarationRanges where
   range          : DeclarationRange
   selectionRange : DeclarationRange
   deriving Inhabited, Repr
 
+instance : ToExpr DeclarationRanges where
+  toExpr r   := mkAppN (mkConst ``DeclarationRanges.mk) #[toExpr r.range, toExpr r.selectionRange]
+  toTypeExpr := mkConst ``DeclarationRanges
+
+builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) ← IO.mkRef {}
 builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ← mkMapDeclarationExtension `declranges
 
+def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRanges) : IO Unit :=
+  builtinDeclRanges.modify (·.insert declName declRanges)
+
 def addDeclarationRanges [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) : m Unit :=
   modifyEnv fun env => declRangeExt.insert env declName declRanges
 
 def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
   return declRangeExt.find? (← getEnv) declName
 
-def findDeclarationRanges? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) := do
+def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m (Option DeclarationRanges) := do
+  if let some ranges := (← builtinDeclRanges.get (m := IO)).find? declName then
+    return ranges
   let env ← getEnv
   if isAuxRecursor env declName || isNoConfusion env declName || (← isRec declName)  then
     findDeclarationRangesCore? declName.getPrefix
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 8d66251d4d..cc28a5b85b 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -9,6 +9,7 @@ import Lean.Parser.Extension
 import Lean.KeyedDeclsAttribute
 import Lean.Elab.Exception
 import Lean.DocString
+import Lean.DeclarationRange
 import Lean.Compiler.InitAttr
 
 namespace Lean
@@ -105,8 +106,10 @@ unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (
     evalKey       := fun _ stx => syntaxNodeKindOfAttrParam parserNamespace stx
     onAdded       := fun builtin declName => do
       if builtin then
-        if let some doc ← findDocString? (← getEnv) declName then
-          declareBuiltin declName (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
+      if let some doc ← findDocString? (← getEnv) declName 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])
   } attrDeclName
 
 unsafe def mkMacroAttributeUnsafe : IO (KeyedDeclsAttribute Macro) :=
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 2bb7fe8f39..031751a827 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -9,6 +9,7 @@ import Lean.Parser.Basic
 import Lean.Parser.StrInterpolation
 import Lean.KeyedDeclsAttribute
 import Lean.DocString
+import Lean.DeclarationRange
 
 /-! Extensible parsing via attributes -/
 
@@ -451,7 +452,9 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
     declareLeadingBuiltinParser catName declName prio
   | _ => throwError "unexpected parser type at '{declName}' (`Parser` or `TrailingParser` expected)"
   if let some doc ← findDocString? (← getEnv) declName then
-    declareBuiltin declName (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
+    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])
   runParserAttributeHooks catName declName (builtin := true)
 
 /-