search

ocaml-gospel / gospel

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

Comments can break preprocessing #320

Closed shym closed 1 year ago

shym commented 1 year ago 
(*@ type t *)
(*@ ephemeral *)

is correctly preprocessed into:

[@@@gospel
 {| type t |}[@@gospel
 {| ephemeral |}]
               ]

(note the nesting) but

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

is preprocessed into:

[@@@gospel {| type t |} ] (* some type *)
[@@gospel {| ephemeral |} ]

which is not properly nested (and not correct OCaml syntax).

This is breaking quite a few examples from the documentation.