On 2017-05-17 05:43, Santiago Zanella wrote: > fsdoc comments need not be attached to a definition. You can > use a `(** ... **)`-style comment for sectioning by leaving an > empty line after it (…). 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.
Makes sense, thanks. I was misled by the fact that the interactive mode rejects naked doc comments. Do you have an opinion on title markers? > On Wed, May 17, 2017 at 7:44 AM, Clément Pit-Claudel via fstar-club > <fstar-club@lists.gforge.inria.fr <mailto: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 <mailto:fstar-club@lists.gforge.inria.fr> > https://lists.gforge.inria.fr/mailman/listinfo/fstar-club > <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
