Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Add handling for double underscores #127

Merged
merged 7 commits into from
Sep 25, 2023
Merged

Conversation

tirix
Copy link
Collaborator

@tirix tirix commented Sep 24, 2023

This is to align with change done in metamath/metamath-exe#160, to handle cases discovered in metamath/set.mm#3389.

Before these changes, double underscores were treated as subscript. They are now correctly ignored and returned as a single span.

To be complete, in addition to these changes, the unescape_text function in CommentItem should also transform double underscores into single underscores. @digama0, what's your proposal for those?

@tirix tirix requested a review from digama0 September 24, 2023 22:49
@digama0
Copy link
Member

digama0 commented Sep 25, 2023

@tirix I made a modification here to inline get_underscore_mode since the advantage of having a separate function is reduced if it is not using ? anymore, but maybe the new code is a bit too terse. LMK what you think.

@tirix
Copy link
Collaborator Author

tirix commented Sep 25, 2023

@tirix I made a modification here to inline get_underscore_mode since the advantage of having a separate function is reduced if it is not using ? anymore, but maybe the new code is a bit too terse. LMK what you think.

Yes indeed, and there is no need for a special enum for that. Ok with the change.

@digama0 digama0 merged commit 4103ee4 into metamath:main Sep 25, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants