Option to align a comment's opening and closing stars

[mjambon]

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.