search

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

Consider comments as spaces while preprocessing #321

Closed shym closed 1 year ago

shym commented 1 year ago

In the following specification:

(*@ type t *)
(*@ ephemeral *)

the preprocessor needs to recognize that ephemeral must be attached in a nested attribute to the first attribute containing type t. It does so by accepting Space between the two items, but not simple comments.

So this turn simple comments into another form of Space so that

(*@ type t *) (* a ghost type *)
(*@ ephemeral *)

is valid syntax.

Closes #320 (hopefully)

shym commented 1 year ago

Where would you expect this to be documented? Maybe this would be fixed as part of a #324 fix?

n-osborne commented 1 year ago

331 add support for

(*@ type t *)
(** documentation *)
(@ ephemeral *)

with any number of newline characters between the ghost declaration and its specification.

n-osborne commented 1 year ago

This just need an entry in the changelog and it is good to be merged.

shym commented 1 year ago

I added a CHANGES entry and CI is happy, so I merged.