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

Refactoring printers #3425

Merged
merged 11 commits into from
Aug 30, 2024
Merged

Refactoring printers #3425

merged 11 commits into from
Aug 30, 2024

Conversation

mtzguido
Copy link
Member

Internally, the pretty printer and ugly printer are interconnected and sometimes hard to update. Plus, the ugly printer's output is parsed by Vale, so it must adhere to a given shape which makes it hard to update, or to do other changes (e.g. see the need for this patch be3f709 in #3406).

This PR separates them and moves to using typeclasses almost everywhere. Next, I will do a Vale printer so we can fully isolate the output needed by Vale. But this is a big change already and I'd like to merge it.

Please report if you find any error messages have changed for the worse.

@mtzguido mtzguido merged commit 86be6d1 into FStarLang:master Aug 30, 2024
2 checks passed
@mtzguido mtzguido deleted the printers branch August 30, 2024 07:46
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.

1 participant