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

Handling inline comments outside the main verus-body #18

Open
parno opened this issue Dec 18, 2023 · 0 comments
Open

Handling inline comments outside the main verus-body #18

parno opened this issue Dec 18, 2023 · 0 comments
Labels
bug Something isn't working enhancement New feature or request

Comments

@parno
Copy link
Contributor

parno commented Dec 18, 2023

The main parse_and_format has special handling for top-level comments and items, but this means those items don't benefit from/share code with the main formatting logic in to_doc. For example, when we process this code:

verus! {

pub type ReplicaId = usize; // $line_count$Trusted$

} // verus!

It gets parsed as a top-level type_alias item followed by a comment that gets treated as a top-level suffix comment in parse_and_format, which means we don't notice that it's been flagged as an inline comment. We could replicate that logic in parse_and_format, but I suspect we should instead try to simplify parse_and_format and rely more consistently on to_doc.

@jaybosamiya jaybosamiya added enhancement New feature or request bug Something isn't working labels Dec 29, 2023
@parno parno changed the title Handling inline comments Handling inline comments outside the main verus-body Feb 7, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants