I didn't find an option to align the stars of closing comments. It's intended for comments that use a star at the beginning of each line, like this:
(* hello
* world
*)
The closing delimiter currently gets indented as follows by ocp-indent, which looks bad:
(* hello
* world
*)
This happens regardless the strict_comments setting.
Option 1
I propose adding a setting for aligning the opening star with the closing star when the closing delimiter is on its own line. This would be done independently of what the comment contains. It would produce this:
(* hello
* world
*)
(*
* hello
* world
*)
(* hello
world
*)
(*
hello
world
*)
(* hello world *)
(* hello
world *)
Option 2
Alternatively, if it's easy enough, we could only align the closing star if all the lines of the comment start with a star. This could be done by default without a special setting, and assume the old behavior is a bug. It would give this:
(* hello
*)
(*
hello
*)
(*
* hello
*)
(*
* hello
* world
*)
(*
hello:
* world
* other
*)
Does it seem like a reasonable thing to add? Option 2 seems nicer for the user, being all automatic and accommodating multiple styles.
I didn't find an option to align the stars of closing comments. It's intended for comments that use a star at the beginning of each line, like this:
The closing delimiter currently gets indented as follows by
ocp-indent
, which looks bad:This happens regardless the
strict_comments
setting.Option 1
I propose adding a setting for aligning the opening star with the closing star when the closing delimiter is on its own line. This would be done independently of what the comment contains. It would produce this:
Option 2
Alternatively, if it's easy enough, we could only align the closing star if all the lines of the comment start with a star. This could be done by default without a special setting, and assume the old behavior is a bug. It would give this:
Does it seem like a reasonable thing to add? Option 2 seems nicer for the user, being all automatic and accommodating multiple styles.