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

Isabelle/HOL translation: comments #2974

Merged
merged 9 commits into from
Sep 2, 2024
Merged

Isabelle/HOL translation: comments #2974

merged 9 commits into from
Sep 2, 2024

Conversation

lukaszcz
Copy link
Collaborator

@lukaszcz lukaszcz commented Aug 27, 2024 •
edited
Loading

@lukaszcz lukaszcz added this to the 0.6.6 milestone Aug 27, 2024
@lukaszcz lukaszcz self-assigned this Aug 27, 2024
@lukaszcz lukaszcz mentioned this pull request Aug 28, 2024
Open
5 tasks
@lukaszcz lukaszcz added the enhancement New feature or request label Aug 28, 2024
@lukaszcz lukaszcz marked this pull request as ready for review August 29, 2024 14:18
janmasrovira
janmasrovira reviewed Aug 30, 2024
View reviewed changes
Copy link
Collaborator

@janmasrovira janmasrovira left a comment

Choose a reason for hiding this comment

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

Did you consider ExactPrint?

@lukaszcz
Copy link
Collaborator Author

Did you consider ExactPrint?

No, how does it work? Can I control it to print comments in a specified format and not print them in certain places?

@janmasrovira
Copy link
Collaborator

The idea is that every time you print something you attach a location to that. Then the effect takes care of automatically inserting the comments in the correct place.

If you want to put comments only in certain places, it could be done by providing the location in those places and omiting it everywhere else.

@lukaszcz
Copy link
Collaborator Author

Then the effect takes care of automatically inserting the comments in the correct place.

Depends on the details of what the "correct place" is understood to be. In Isabelle/HOL comments cannot appear inside internal syntax, but I still want to print them at the earliest possible point. Maybe let's discuss this on Monday.

lukaszcz and others added 9 commits September 2, 2024 13:47
@lukaszcz
translate locations
25fb478
@lukaszcz
HasLoc
ea810db
@lukaszcz
comments
57d6e5d
@lukaszcz
ppComments
8fe8459
@lukaszcz
locations
668ba42
@lukaszcz
fix comments
00e8b68
@lukaszcz
fix comment locations
6029607
@lukaszcz
fix tests
b92c13a
@janmasrovira @lukaszcz
Separate Comment from pretty Options (#2988)
b2faa3d 
I think it makes more sense to not have `State Options` as they are
supposed to be immutable and have a separate `Input` effect for
comments.
@lukaszcz lukaszcz merged commit b9d8641 into main Sep 2, 2024
4 checks passed
@lukaszcz lukaszcz deleted the isabelle-comments branch September 2, 2024 13:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@janmasrovira janmasrovira janmasrovira approved these changes

@paulcadman paulcadman Awaiting requested review from paulcadman

Assignees

@lukaszcz lukaszcz

Labels
enhancement New feature or request isabelle
Projects
None yet
Milestone
0.6.6
Development

Successfully merging this pull request may close these issues.

Include comments in the Isabelle/HOL translation
2 participants
@lukaszcz @janmasrovira