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

Fix: pprint positive kw for data types #1980

Merged
merged 5 commits into from
Apr 5, 2023
Merged

Fix: pprint positive kw for data types #1980

merged 5 commits into from
Apr 5, 2023

Conversation

jonaprieto
Copy link
Collaborator

@jonaprieto jonaprieto commented Apr 5, 2023

As the title says.

  • I found this bug while formatting the examples found in the tests folder.

  • In addition to printing the missing positive' keyword for data types, the code also prints certain keyword annotations onto separate lines, the ones that act as attributes to their term. While this is a matter of personal preference, I find that it makes it easier to comment and uncomment individual annotations.

@jonaprieto jonaprieto requested a review from janmasrovira April 5, 2023 10:03
@jonaprieto jonaprieto added this to the 0.3.2 milestone Apr 5, 2023
@jonaprieto jonaprieto marked this pull request as ready for review April 5, 2023 11:01
@jonaprieto jonaprieto temporarily deployed to github-pages April 5, 2023 11:08 — with GitHub Actions Inactive
@jonaprieto jonaprieto requested review from paulcadman and removed request for janmasrovira April 5, 2023 11:18
@jonaprieto jonaprieto self-assigned this Apr 5, 2023
@paulcadman
Copy link
Collaborator

Printing keyword annotations onto separate lines probably requires more discussion.

My opinion is that it's inconsistent with other keywords. For example we don't format module, infix or type like:

module
Foo;
infix 6
+;
type
Foo := | foo;

@jonaprieto
Copy link
Collaborator Author

Sure! open discussion

it's inconsistent with other keywords

My preference for this formatting is based on the fact that it can be helpful when refactoring or testing code. When each annotation is commented on its line, it becomes easier to modify them without affecting the rest of its terms. Like minimizing the diff mark. Also, in each case you mentioned, if you were to comment or uncomment the corresponding keyword line, it would effectively render the statement invalid. Annotations like terminating, builtins, or even axioms act as attributes to the term, and they may be removed later.

@jonaprieto jonaprieto added the enhancement New feature or request label Apr 5, 2023
@paulcadman
Copy link
Collaborator

OK - let's do it 🚀 !

Suggestion: Update the language reference formatting:

@jonaprieto
Copy link
Collaborator Author

Done, I updated the excerpts in the documentation I saw. Likely, I forgot some, so we need to review the format later, so I'll leave this for another pr if it's ok with you.

@jonaprieto jonaprieto temporarily deployed to github-pages April 5, 2023 13:29 — with GitHub Actions Inactive
@jonaprieto jonaprieto merged commit 7431d80 into main Apr 5, 2023
@jonaprieto jonaprieto deleted the fix-bug-formatter branch April 5, 2023 14:40
@janmasrovira janmasrovira mentioned this pull request Apr 5, 2023
@jonaprieto jonaprieto restored the fix-bug-formatter branch April 6, 2023 10:46
jonaprieto added a commit that referenced this pull request Apr 12, 2023
This PR fixes a formatting issue that drops blank lines between axiom
declarations.

It goes after:

- #1980
- Closes #1986
@jonaprieto jonaprieto deleted the fix-bug-formatter branch October 5, 2023 12:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants