This PR makes the automatic first token detection in tactic docs much
more robust, in addition to making it work in modules and other contexts
where builtin tactics are not in the environment. It also adds the
ability to override the tactic's first token as the user-visible name.
Previously, first token detection would look up the parser descriptor in
the environment and process its syntax. This would be incorrect for
builtin parsers, as well as for modules in which the definition is not
loaded. Now, it instead consults the Pratt parsing table for the
`tactic` syntax category. Tests are added that ensure this keeps working
in modules, and also that the first token of all tactics that ship with
Lean are either detected unambiguously or annotated to remove ambiguity.
Closes#12038.
This PR significantly improves the test coverage of the language server,
providing at least a single basic test for every request that is used by
the client. It also implements infrastructure for testing all of these
requests, e.g. the ability to run interactive tests in a project context
and refactors the interactive test runner to be more maintainable.
Finally, it also fixes a small bug with the recently implemented unknown
identifier code actions for auto-implicits (#10442) that was discovered
in testing, where the "import all unambiguous unknown identifiers" code
action didn't work correctly on auto-implicit identifiers.
This PR fixes a bug in structure instance field completion that caused
it to not function correctly for bracketed structure instances written
in Mathlib style.
This PR enables tactic completion in the whitespace of a tactic proof
and adds tactic docstrings to the completion menu.
Future work:
- A couple of broken tactic completions: This is due to tactic
completion now using @david-christiansen's `Tactic.Doc.allTacticDocs` to
obtain the tactic docstrings and should be fixed soon.
- Whitespace tactic completion in tactic combinators: This requires
changing the syntax of tactic combinators to produce a syntax node that
makes it clear that a tactic is expected at the given position.
Closes#1651.
