Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Parse pluscal labels inserted due to macro #353

Merged
merged 2 commits into from
Dec 20, 2024

Conversation

hwayne
Copy link
Contributor

@hwayne hwayne commented Dec 12, 2024

Fixes #352

image

Since parsing rules for label insertions due to macros are slightly different than parsing any other location in the translation output, I figured it would work best to add a separate parseLabelLocation method with different rules. See docstring for an explanation as to differences.

Signed-off-by: Hillel <h@hillelwayne.com>
@@ -124,21 +125,25 @@ export class TranspilerStdoutParser extends ProcessOutputHandler<DCollection> {
return false;
}

const matcher = /^\s\s([A-Za-z0-9_]+) at line \d+, column \d+$/g.exec(line);
const matcher = /^\s\s([A-Za-z0-9_]+) at line \d+, column \d+/g.exec(line);
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note the removal of the $ at the end, so it will match as long as the string has matcher as a prefix. This is only called if we're in label parsing mode so won't affect parsing any other output.

*/

private parseLabelLocation(line: string): LocationInfo | undefined {
const rxLocation = /\s*(?:at )?line (\d+), column (\d+)(?: of macro called at line (\d+), column (\d+))?.?\s*/g; // no closing `$`
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think removing the $ is actually necessary here; if everything else in the PR looks okay I can test and possibly remove this comment.

@hwayne
Copy link
Contributor Author

hwayne commented Dec 12, 2024

Also, I checked procedure label insertion just to be sure. They work fine.

Copy link
Collaborator

@FedericoPonzi FedericoPonzi left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, thanks!

Signed-off-by: Hillel <h@hillelwayne.com>
@hwayne
Copy link
Contributor Author

hwayne commented Dec 20, 2024

Comment moved, ready to merge!

@FedericoPonzi FedericoPonzi merged commit c077132 into tlaplus:master Dec 20, 2024
4 checks passed
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

"Show inserted labels" diagnostics don't work when a label is inserted via macro
2 participants