feature request: formatting and controlling line in goal view

[oddcoder]

So this is two feature requests actually,

The first is to have line split + indendetation at ever -> or <-> it makes folowing the goals a bit easier, for instance compare the following formattings side by side:

The second thing is to always keep the goal in the viewable part of the buffer, for isntance, somtimes i have lots of assumptions, and I end up having to scroll to the bottom of the goal to see the what I am proving as in this example:

It is more ergonomic if the focus (not sure if I am using the right terminology) is on the first goal instead of the asumptions.

[tomtomjhj]

Hi, thanks for suggestions.

1. formatting

I believe VsCoq on VS Code doesn't support this either. The older Coq server (coqidetop, used by Coqtail) used to send the terms pretty-printed, but vscoqtop (used by vscoq.nvim and VsCoq 2) sends the terms without much formatting. While it would be possible to implement some ad-hoc prettification in vscoq.nvim, I think this should be handled by the server since it can utilize the existing logic for pretty printing.

I'm a bit busy now, so I suggest you to check if the VsCode client behaves similarly, and if so please raise an issue on the vscoq repository.

2. focus

That sounds like a good idea.

Some points for discussion:

1. What should be the default behavior?
   1. always put the hypotheses-goal separator (====) at the center of window (zz)
   2. give the maximum space to the goal (so that if the goal is huge, the hypotheses are outside the viewport)
2. Currently vscoq.nvim restores the view (the first visible line, cursor position, etc; see:h winsaveview) when proofview is updated (e.g., when moving the cursor to the next sentence). This is useful if the goal is huge (typical when working with Iris-based projects), in which case resetting the focus would be a worse option. So I would like to have both focus-to-first-goal and restore-view behaviors, but atm I'm not quite sure how they should interact. I'll think about it when I have some time.

[oddcoder]

I agree regarding formatting I talked to vscoq folks, and thy acknowledge the issue.

Regarding Focusing: in my opinion the most productive view is to view as much of the current goal as possible but no more. So:

• If the goal is very small, we can show the goal, the separator (=====) and all the hypothesis.
• If there are too many hypotheses, to fit in on page, then the goal would be at the bottom of the page, but still fully viewable without scrolling.
• If the goal itself is too big to place in on page, then the page should contain the goal starting from the spearator(===)

I am not sure if this is the best way to view things, and I am not expert enough with vim to understand how complex or trivial this might be. But it feels the most natural to me.