diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean
index 175d9f31b9..b0162f651b 100644
--- a/src/Lean/Linter/MissingDocs.lean
+++ b/src/Lean/Linter/MissingDocs.lean
@@ -19,111 +19,169 @@ register_builtin_option linter.missingDocs : Bool := {
 
 def getLinterMissingDocs (o : Options) : Bool := getLinterValue linter.missingDocs o
 
+
+namespace MissingDocs
+
+abbrev SimpleHandler := Syntax → CommandElabM Unit
+abbrev Handler := Bool → SimpleHandler
+
+unsafe def mkHandlerUnsafe (constName : Name) : ImportM Handler := do
+  let env  := (← read).env
+  let opts := (← read).opts
+  match env.find? constName with
+  | none      => throw ↑s!"unknown constant '{constName}'"
+  | some info => match info.type with
+    | Expr.const ``SimpleHandler _ => do
+      let h ← IO.ofExcept $ env.evalConst SimpleHandler opts constName
+      pure fun enabled stx => if enabled then h stx else pure ()
+    | Expr.const ``Handler _ =>
+      IO.ofExcept $ env.evalConst Handler opts constName
+    | _ => throw ↑s!"unexpected missing docs handler at '{constName}', `MissingDocs.Handler` or `MissingDocs.SimpleHandler` expected"
+
+@[implementedBy mkHandlerUnsafe]
+opaque mkHandler (constName : Name) : ImportM Handler
+
+builtin_initialize missingDocsExt :
+  PersistentEnvExtension (Name × Name) (Name × Name × Handler) (List (Name × Name) × NameMap Handler) ←
+  registerPersistentEnvExtension {
+    name            := "missing docs extension"
+    mkInitial       := pure ([], {})
+    addImportedFn   := fun as =>
+      ([], ·) <$> as.foldlM (init := {}) fun s as =>
+        as.foldlM (init := s) fun s (n, k) => s.insert k <$> mkHandler n
+    addEntryFn      := fun (entries, s) (n, k, h) => ((n, k)::entries, s.insert k h)
+    exportEntriesFn := fun s => s.1.reverse.toArray
+    statsFn := fun s => format "number of local entries: " ++ format s.1.length
+  }
+
+def addHandler (env : Environment) (declName key : Name) (h : Handler) : Environment :=
+  missingDocsExt.addEntry env (declName, key, h)
+
+def getHandlers (env : Environment) : NameMap Handler := (missingDocsExt.getState env).2
+
 partial def missingDocs : Linter := fun stx => do
-  go (getLinterMissingDocs (← getOptions)) stx
-where
-  lint (stx : Syntax) (msg : String) : CommandElabM Unit :=
-    logWarningAt stx s!"missing doc string for {msg} [linter.missingDocs]"
+  if let some h := (getHandlers (← getEnv)).find? stx.getKind then
+    h (getLinterMissingDocs (← getOptions)) stx
 
-  lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
-    lint stx s!"{msg} {stx.getId}"
+builtin_initialize
+  let name := `missingDocsHandler
+  registerBuiltinAttribute {
+    name
+    descr := "adds a syntax traversal for the missing docs linter"
+    applicationTime := .afterCompilation
+    add := fun declName stx kind => do
+      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
+      let env ← getEnv
+      unless (env.getModuleIdxFor? declName).isNone do
+        throwError "invalid attribute '{name}', declaration is in an imported module"
+      let decl ← getConstInfo declName
+      let fnNameStx ← Attribute.Builtin.getIdent stx
+      let key ← Elab.resolveGlobalConstNoOverloadWithInfo fnNameStx
+      unless decl.levelParams.isEmpty && (decl.type == .const ``Handler [] || decl.type == .const ``SimpleHandler []) do
+        throwError "unexpected missing docs handler at '{declName}', `MissingDocs.Handler` or `MissingDocs.SimpleHandler` expected"
+      setEnv <| missingDocsExt.addEntry env (declName, key, ← mkHandler declName)
+  }
 
-  lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
-    lint stx s!"{msg} {parent.getId}.{stx.getId}"
+def lint (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  logWarningAt stx s!"missing doc string for {msg} [linter.missingDocs]"
 
-  go (enabled : Bool) : Syntax → CommandElabM Unit
-  | stx@(Syntax.node _ k args) => do
-    match k with
-    | ``«in» =>
-      if stx[0].getKind == ``«set_option» then
-        let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
-        withScope (fun scope => { scope with opts }) do
-          go (getLinterMissingDocs opts) stx[2]
-      else
-        go enabled stx[2]
-      return
-    | ``«mutual» =>
-      args[1]!.getArgs.forM (go enabled)
-      return
-    | _ => unless enabled do return
-    match k with
-    | ``declaration =>
-      let #[head, rest] := args | return
-      if head[2][0].getKind == ``«private» then return -- not private
-      if head[0].isNone then -- no doc string
-        match rest.getKind with
-        | ``«abbrev» => lintNamed rest[1][0] s!"public abbrev"
-        | ``«def» => lintNamed rest[1][0] "public def"
-        | ``«opaque» => lintNamed rest[1][0] "public opaque"
-        | ``«axiom» => lintNamed rest[1][0] "public axiom"
-        | ``«inductive» => lintNamed rest[1][0] "public inductive"
-        | ``classInductive => lintNamed rest[1][0] "public inductive"
-        | ``«structure» => lintNamed rest[1][0] "public structure"
-        | _ => pure ()
-      if rest.getKind matches ``«inductive» | ``classInductive then
-        for stx in rest[4].getArgs do
-          let head := stx[1]
-          if head[2][0].getKind != ``«private» && head[0].isNone then
-            lintField rest[1][0] stx[2] "public constructor"
-        unless rest[5].isNone do
-          for stx in rest[5][0][1].getArgs do
-            let head := stx[0]
-            if head[2][0].getKind == ``«private» then return -- not private
-            if head[0].isNone then -- no doc string
-              lintField rest[1][0] stx[1] "computed field"
-      else if rest.getKind == ``«structure» then
-        unless rest[5].isNone || rest[5][2].isNone do
-          for stx in rest[5][2][0].getArgs do
-            let head := stx[0]
-            if head[2][0].getKind != ``«private» && head[0].isNone then
-              if stx.getKind == ``structSimpleBinder then
-                lintField rest[1][0] stx[1] "public field"
-              else
-                for stx in stx[2].getArgs do
-                  lintField rest[1][0] stx "public field"
-    | ``«initialize» =>
-      let #[head, _, rest, _] := args | return
-      if rest.isNone then return
+def lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  lint stx s!"{msg} {stx.getId}"
+
+def lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
+  lint stx s!"{msg} {parent.getId}.{stx.getId}"
+
+def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do
+  if k == ``«abbrev» then lintNamed id s!"public abbrev"
+  else if k == ``«def» then lintNamed id "public def"
+  else if k == ``«opaque» then lintNamed id "public opaque"
+  else if k == ``«axiom» then lintNamed id "public axiom"
+  else if k == ``«inductive» then lintNamed id "public inductive"
+  else if k == ``classInductive then lintNamed id "public inductive"
+  else if k == ``«structure» then lintNamed id "public structure"
+
+def checkDecl (args : Array Syntax) : CommandElabM Unit := do
+  let #[head, rest] := args | return
+  if head[2][0].getKind == ``«private» then return -- not private
+  let k := rest.getKind
+  if head[0].isNone then -- no doc string
+    lintDeclHead k rest[1][0]
+  if k == ``«inductive» || k == ``classInductive then
+    for stx in rest[4].getArgs do
+      let head := stx[1]
       if head[2][0].getKind != ``«private» && head[0].isNone then
-        lintNamed rest[0] "initializer"
-    | ``«syntax» =>
-      if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
-        if stx[5].isNone then lint stx[3] "syntax"
-        else lintNamed stx[5][0][3] "syntax"
-    | ``syntaxAbbrev =>
-      if stx[0].isNone then
-        lintNamed stx[2] "syntax"
-    | ``syntaxCat =>
-      if stx[0].isNone then
-        lintNamed stx[2] "syntax category"
-    | ``«macro» =>
-      if stx[0].isNone && stx[1][0][0].getKind != ``«local» then
-        if stx[4].isNone then lint stx[2] "macro"
-        else lintNamed stx[4][0][3] "macro"
-    | ``«elab» =>
-      if stx[0].isNone && stx[1][0][0].getKind != ``«local» then
-        if stx[4].isNone then lint stx[2] "elab"
-        else lintNamed stx[4][0][3] "elab"
-    | ``classAbbrev =>
-      let head := stx[0]
-      if head[2][0].getKind != ``«private» && head[0].isNone then
-        lintNamed stx[3] "class abbrev"
-    | ``Parser.Tactic.declareSimpLikeTactic =>
-      if stx[0].isNone then
-        lintNamed stx[3] "simp-like tactic"
-    | ``Option.registerBuiltinOption =>
-      if stx[0].isNone then
-        lintNamed stx[2] "option"
-    | ``Option.registerOption =>
-      if stx[0].isNone then
-        lintNamed stx[2] "option"
-    | ``registerSimpAttr =>
-      if stx[0].isNone then
-        lintNamed stx[2] "simp attr"
-    | ``Elab.Tactic.configElab =>
-      if stx[0].isNone then
-        lintNamed stx[2] "config elab"
-    | _ => return
-  | _ => return
+        lintField rest[1][0] stx[2] "public constructor"
+    unless rest[5].isNone do
+      for stx in rest[5][0][1].getArgs do
+        let head := stx[0]
+        if head[2][0].getKind == ``«private» then return -- not private
+        if head[0].isNone then -- no doc string
+          lintField rest[1][0] stx[1] "computed field"
+  else if rest.getKind == ``«structure» then
+    unless rest[5].isNone || rest[5][2].isNone do
+      for stx in rest[5][2][0].getArgs do
+        let head := stx[0]
+        if head[2][0].getKind != ``«private» && head[0].isNone then
+          if stx.getKind == ``structSimpleBinder then
+            lintField rest[1][0] stx[1] "public field"
+          else
+            for stx in stx[2].getArgs do
+              lintField rest[1][0] stx "public field"
+
+def main (stx : Syntax) (k : SyntaxNodeKind) (args : Array Syntax) : CommandElabM Unit := do
+  if k == ``declaration then
+    checkDecl args
+  else if k == ``«initialize» then
+    let #[head, _, rest, _] := args | return
+    if rest.isNone then return
+    if head[2][0].getKind != ``«private» && head[0].isNone then
+      lintNamed rest[0] "initializer"
+  else if k == ``«syntax» then
+    if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+      if stx[5].isNone then lint stx[3] "syntax"
+      else lintNamed stx[5][0][3] "syntax"
+  else if k == ``syntaxAbbrev then
+    if stx[0].isNone then
+      lintNamed stx[2] "syntax"
+  else if k == ``syntaxCat then
+    if stx[0].isNone then
+      lintNamed stx[2] "syntax category"
+  else if k == ``«macro» then
+    if stx[0].isNone && stx[1][0][0].getKind != ``«local» then
+      if stx[4].isNone then lint stx[2] "macro"
+      else lintNamed stx[4][0][3] "macro"
+  else if k == ``«elab» then
+    if stx[0].isNone && stx[1][0][0].getKind != ``«local» then
+      if stx[4].isNone then lint stx[2] "elab"
+      else lintNamed stx[4][0][3] "elab"
+  else if k == ``classAbbrev then
+    let head := stx[0]
+    if head[2][0].getKind != ``«private» && head[0].isNone then
+      lintNamed stx[3] "class abbrev"
+  else if k == ``Parser.Tactic.declareSimpLikeTactic then
+    if stx[0].isNone then
+      lintNamed stx[3] "simp-like tactic"
+  else if k == ``Option.registerBuiltinOption then
+    if stx[0].isNone then
+      lintNamed stx[2] "option"
+  else if k == ``Option.registerOption then
+    if stx[0].isNone then
+      lintNamed stx[2] "option"
+  else if k == ``registerSimpAttr then
+    if stx[0].isNone then
+      lintNamed stx[2] "simp attr"
+  else if k == ``Elab.Tactic.configElab then
+    if stx[0].isNone then
+      lintNamed stx[2] "config elab"
+  else return
+
+def handleIn : Handler := fun _ stx => do
+  if stx[0].getKind == ``«set_option» then
+    let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
+    withScope (fun scope => { scope with opts }) do
+      missingDocs stx[2]
+
+def handleMutual : Handler := fun _ stx => do
+  stx[1].getArgs.forM missingDocs
 
 builtin_initialize addLinter missingDocs