fsdoc comments need not be attached to a definition. You can use a `(** ... **)`-style comment for sectioning by leaving an empty line after it ( https://github.com/FStarLang/FStar/wiki/Generating-documentation-with-fsdoc-comments). I regularly do so, and that is why some of the sectioning comments you see that use that style don't result in parsing errors.
I dislike the syntactic-restrictions of fsdoc comments (re empty lines). The parsing errors that one gets when not respecting these restrictions are very annoying. I'm in favor of having something more like coqdoc. On Wed, May 17, 2017 at 7:44 AM, Clément Pit-Claudel via fstar-club < fstar-club@lists.gforge.inria.fr> wrote: > 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 >
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
