whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
274 stars 34 forks source link

Is there a way to change indentation style? #246

Closed ju-sh closed 2 years ago

ju-sh commented 2 years ago

By default coqtail seems to indent 'branches' (not sure if that's the right term) like

Inductive exmpl :=
  | hi
  | hello.

with an indentation level before the |s.

Even if we try to remove the indentation, the next 'branch' would retain the same indentation level (probably how it's supposed to work) like

Inductive exmpl :=
  | hi

changed to

Inductive exmpl :=
| hi

becoming

Inductive exmpl :=
| hi
  |

on hitting beginning to write a new line.

Is there a way to set the default indentation style to one without spaces before the |s? Like

Inductive exmpl :=
| hi
| hello.

I'm on:

whonore commented 2 years ago

There is not currently an option to control that, but it should be relatively easy to add so I'll try to do that soon.

whonore commented 2 years ago

The PR I just merged added an option called g:coqtail_inductive_shift that should do what you want if you set it to 0.

ju-sh commented 2 years ago

Thanks, it works!

At first I thought I set the option wrong when I hit enter after typing

Inductive exmpl :=

as the cursor moved to a position after a level of indentation. But when I typed the | it went back.

Inductive exmpl :=
|