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.

Sign up for GitHub

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

Jump to bottom

Use numbers instead of primes to distinguish shadowed saw-core variables. #1636

Merged
merged 2 commits into from
Apr 25, 2022
Merged

Use numbers instead of primes to distinguish shadowed saw-core variables. #1636

merged 2 commits into from
Apr 25, 2022

Conversation

brianhuffman
Copy link
Contributor

Fixes #1619.

Reduce excessive linebreaks when printing large terms.
e16cc8c 
This is accomplished by using a layout with an extremely large
page width, combined with a normal (64-character) ribbon width.
With this setup, the pretty-printer should almost never in practice
go into the bayond-the-margin mode where it prints only one token
per line.

Fixes #1618.
@brianhuffman
Copy link
Contributor Author

The fix for #1618 is conceptually separate, but sort of related in that it has to do with pretty-printing. It seems easier to put them in one PR, but it might be easier to review the commits in the PR separately.

@brianhuffman brianhuffman linked an issue Apr 22, 2022 that may be closed by this pull request
Pretty-printing saw-core syntax results in way too many line-breaks #1618
Closed
@brianhuffman brianhuffman requested a review from chameco April 22, 2022 19:11
chameco
chameco approved these changes Apr 24, 2022
View reviewed changes
Copy link
Contributor

@chameco chameco left a comment

Choose a reason for hiding this comment

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

This looks good - I think it's fine to bundle the #1618 fix, as both are related specifically to readability of the pretty-printed output.

@brianhuffman brianhuffman added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Apr 25, 2022
@brianhuffman brianhuffman merged commit c0b2da9 into master Apr 25, 2022
@mergify mergify bot deleted the shadowed-var-numbers branch April 25, 2022 14:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@chameco chameco chameco approved these changes

@eddywestbrook eddywestbrook Awaiting requested review from eddywestbrook

Assignees
No one assigned
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run
Projects
None yet
Milestone
No milestone
2 participants
@brianhuffman @chameco