-
Notifications
You must be signed in to change notification settings - Fork 52
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add configurable prefixes for custom label commands. (#1139)
This commit extends the configs with a map from label command name to the respective prefix: * Prepends user-defined prefixes to labels in the semantics pass. Note that this yields to a mismatch between the actual length of a span and its range, but there are no (anticipated) bad side-effects due to this. * Adds two tests that ensure completion for custom labels with custom prefix works as expected. The `\ref` command should list the prefix, while a custom reference command with a configured prefix should not. * Implements key functionality for renaming labels with prefixes. A sane assumption it does is that all labels found as candidate for renaming share a common prefix, up to looking it up first and prepending it, e.g., for `\goal{foo}`. Instead of storing a renaming candidate for each entry, it only keeps track of the prefixes and prepends them accordingly, depending on the renaming candidate, by swapping the `TextRange` with `RenameInformation` inside the `RenameResult`. Unfortunately, this pollutes a bit the other renaming ops, such as commands or citations, which don't have prefixes. Nevertheless, changes there have been incremental and `RenameInformation` implements a `From<TextRange>` to easily map an existing `TextRange` into it, simply assuming an empty prefix. In terms of tests, the `prefix` should be ignored.
- Loading branch information
Showing
17 changed files
with
529 additions
and
40 deletions.
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.