feat: make MissingDocs extensible

[digama0]

This should also fix the compile time cost issue noticed in #1390. This adds an environment extension and attribute to add MissingDocs.Handlers for user-defined commands, so that they can also be docs linted. The only thing you have to do in a handler is identify if there is a docstring on the syntax, and if not then call the lintNamed function with the span of the new identifier.

You can implement either Handler or SimpleHandler:

• SimpleHandler := Syntax -> CommandElabM Unit gets the syntax of the command and possibly reports a lint warning. It is only called if the syntax has the syntax kind specified in the attribute, and if the missingDocs linter itself is enabled.
• Handler := Bool -> Syntax -> CommandElabM Unit is called even if the linter is disabled, and is passed the enabled state. This is needed for commands that contain other commands, because nested commands can have a set_option that locally re-enables the linter.

[gebner]

Suggested change

	abbrev SimpleHandler := Syntax → CommandElabM Unit
	abbrev Handler := Bool → SimpleHandler
	abbrev SimpleHandler ks := TSyntax ks → CommandElabM Unit
	abbrev Handler ks := Bool → SimpleHandler ks

Then we could also drop the foo in @[missingDocsHandler foo].

[digama0]

That makes the evalConst a lot trickier, I think? EDIT: Yeah, I don't want to deal with this. This can be a separate PR, and I probably won't be the one to write it. I think it's already usable enough for practical purposes, and it accomplishes the stated goal of extensibility to declarations outside the core.

[Kha]

Yeah, this is an interesting general refactoring that we can apply to other places as well, especially after strengthening the macro typing story.

[leodemoura]

Merged manually due to stage0 conflicts