Hi all,
`fstar-mode` currently displays certain special comments (`(*** … ***)`, `(*+
+*)`, and `(*! !*)`) in a larger font. There are some uses of this in the
standard library (`(***` is used by a few people, but I could only find one
user of `(+`, and none of `(*!`).
There's one problem with `(***` though: F* understands it as a doc comment and
attaches it to the next definition (and errors if it can't find such a
definition). I can think of two possible fixes:
* Changing the parser to not treat `(***` as a doc comment.
* Changing fstar-mode to use different delimiters. Maybe something like `(* *`,
`(* **`, and `(* ***`? (That's what coqdoc uses.)
The second fix would also nicely address another problem: although doc comments
are documented to attach to the definition that they precede, they are commonly
used e.g. for sectioning. Some examples:
(** **************************************************************** **)
(** Defining a generic 'bytes' type as a view on a sequence of bytes **)
(** **************************************************************** **)
(** Uints to Uints **)
(** some lemmas that summarize the behavior **)
(** Concrete allocators, getters and setters *)
(** Transitivity lemmas *)
I presume this is because `(**` comments get a different highlighting, which
makes them stand out? In any case, blessing a new series of "titling" comment
delimiters (option 2 above) would solve this problem too.
Clément.
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
