Unsatisfactory line break

[ybertot]

In the attached picture the formatting of the last n - 2 is weird.

[gares]

Also,

      (fun x =>
body)

is weird, usually Coq does something like

     (fun x =>
        body)

I don't know which box type is used for fun .. => .., but it seems also .. + .. and .. - .. break forgetting the indentation, so maybe it is the same problem

[tomtomjhj]

It seems vscoq doesn't take account of notation formatting yet.

For example, this is what I get from a big term with Iris notations in Coqtail (using coqidetop) and vscoq2.

Notation definition:

Reserved Notation "P ∗ Q" (at level 80, right associativity, format "P  ∗  '/' Q").

(https://gitlab.mpi-sws.org/iris/iris/-/blob/8a98d00a6ddc25ab6918ee8d216558eaf46b6d53/iris/bi/notation.v#L37)

• vscoq 2.1.7: There is no linebreak after ∗
• Coqtail: It breaks lines after ∗

I wonder if the vscoqtop server can utilize the coqidetop's logic for formatting, which I believe is used here: https://github.com/coq/coq/blob/d6550d16f01d39dee97f7e645e415de51725fd2e/ide/coqide/idetop.ml#L141. If the server implements this functionality, then the client doesn't need to do the complex stuff. (For the context, I'm the author of neovim client for vscoqtop. https://github.com/tomtomjhj/vscoq.nvim)

[TheoWinterhalter]

Related to #859, in particular the discussion which suggests not to reuse coidetop's formatting.

[tomtomjhj]

Oh so the response from vscoqtop does contain the formatting information for notations, but the client isn't fully utilizing that yet.