Multi-line comments formatting

[vzaliva]

When formatting multi-line comment in indented section it should respect current indentation level.
For example, now it formats:

Section Foo.
  (* line 1
line 2
line3 
*)

Expected formatting is something like this:

Section Foo.
  (* line 1
     line 2
     line3 
  *)

[Matafou]

Hi,

I don't know the recommended way of indenting multilines in emacs, but I am pretty sure what you suggest would be an annoyance to many. A lot of people indent there comments by hand (as it is more text than coq) and when reindenting a whole script they certainly don't want there comments to be re-indented.

I am not sure the current behaviour is good either: when commenting one line it behaves more or less like in standard text mode (tries to align with a word on previous line), and when commenting multiple lines it does nothing inside comments.

Maybe we could have a third behaviour when commenting multiple comment-only lines?

[vzaliva]

I only suggest to make it work as it currently works in Java, C, and PHP modes (and probably many others). It is common convention for comments body to respect current indentation level.

I guess you can support old and new behavior with the choice controlled by configuration variable.

[aspiwack]

I'm with @vzaliva: the proposed indentation is more standard. It's also possible to force a particular layout by inserting a character at the beginning of the line:

(*               my
 *        beautifully
 * formatted
 *          layout
 *)

[cpitclaudel]

@aspiwack I don't think this trick will work. If we make indentation work this way, we'll break coqdoc, won't we? Thing like this:

(** Here's some code:
<<
   Definition a :=
     forall x, x > 0 \/ x <= 0.
   Proof.
     intros.
     + blah.
       bluh.
>> *)

IOW, I think we need to either keep things as they are, or make indentation smart enough to recognize these code-in-comments blocks. Or some other idea? @vzaliva, what do you think?

On the other hand

[vzaliva]

Where are two factors here. First is what happen when user press ENTER at the end of the fist comment line. Right now the cursor jumps to the column 0 on the next line. I want it to jump to current indentation level on the next line. This how it works in Java/C/PHP mode.

The second problem how re-indenting of exiting comment works. I suggest that it should only modify comment lines who have non-whitespace characters in columns left of current indentation step by moving them right by current indentation step. Other comment lines which already have whitespace up to indentation step should remain unchanged. That would preserve in-comment formatting.

[cpitclaudel]

I think the RET part is uncontroversial; we should fix this.