ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
126 stars 16 forks source link

fix pps documentation of ghost #331

Closed n-osborne closed 11 months ago

n-osborne commented 1 year ago

This PR add support for the documentation of ghost declarations. Gospel preprocessor should now accept every interleaving of ghost declaration, with and without specification and with or without spaces between these items. Spaces are checked to contains not more than one end of the line character when necessary. Decision has been made (but can obviously been discussed) to support documentation between a ghost declaration and its specification with no constraints on the space in between. (See tests added in the first commit for examples)

Fixes #324

shym commented 11 months ago

I updated this PR with one large modification. Now determining whether space should separate two consecutive items (aka be considered Large) is using data from the lexer (which rules were applied) to handle possibly-nested comments and contained strings properly.

On the way, two minor updates:

shym commented 11 months ago

I just force-pushed an update that only fixes a few typos in a commit message. I’ll merge if CI is happy.