Add a documentation tokens to pps #281
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
n-osborne
force-pushed
the
fix-pps-with-documentation
branch
from
f466a83
to
842097a
Compare
shym
reviewed
Jun 7, 2023
- a Documentation token with positions and contents - an Empty_documentation with just ending position The Empty_documentation token correspond to `(**)`
n-osborne
force-pushed
the
fix-pps-with-documentation
branch
from
842097a
to
e757498
Compare
n-osborne
changed the title
n-osborne
force-pushed
the
fix-pps-with-documentation
branch
from
e757498
to
293ab83
Compare
shym
approved these changes
Jun 30, 2023
n-osborne
force-pushed
the
fix-pps-with-documentation
branch
from
293ab83
to
8126292
Compare
These printers turns the documentation comments into documentation attributes. We will want to use them when the documentation appears between an OCaml declaration and gospel specifications.
Capture all the cases spacing-wise where a documentation comment appears between an OCaml declaration and a gospel specification.
Dune 3 enables cram tests by default
This was referenced Jul 4, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR proposes a fix for #288
It adds two new tokens to the lexer:
Documentationtoken with starting and ending position and the contentsEmpty_documentationtoken with the ending positionBoth are printed as documentation attributes when they appears between an Ocaml declaration and a gospel specification (the case where the documentation comments is considered as detached by the OCaml parser)
Tests are added to check that the documentation is not considered as detached anymore and to make sure that original position is preserved.