[vim] Usability improvements.

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

Apache License 2.0

204 stars 12 forks source link

[vim] Usability improvements. #462

Closed cangiuli closed 5 years ago

cangiuli commented 5 years ago

This contains three improvements to the vim mode.

<LocalLeader>L and <LocalLeader>P add the --ignore-cache option.
Typing <LocalLeader>l or <LocalLeader>L in the redtt output buffer will recheck the most recently checked .red file, if it is still open. (Requested by @jonsterling)
When closing a .red buffer, only close the redtt output buffer if the .red file is the most recently checked one.

favonia commented 5 years ago

I have a separate request: adding a new binder to ignore .rot files ("--ignore-cache"). Maybe <LocalLeader>L?

cangiuli commented 5 years ago

@favonia Done. Right after pushing I realized...do you also want <LocalLeader>P for checking a partial file with --ignore-cache? (It's trivial to add.)

favonia commented 5 years ago

There is no reason for me to say no! LOL

By the way, once redtt becomes mature, maybe we do not need these special keybindings anymore.

jonsterling commented 5 years ago

I'm going to try and test this today; I have only several free minutes though, so we'll see.

jonsterling commented 5 years ago

@cangiuli Is it intentional that when I run \l from inside the output buffer, it moves my cursor to the redtt buffer?

cangiuli commented 5 years ago

Yes, but I could be convinced to implement some other behavior. The problem with staying in the output buffer is that I'm not sure where to place the cursor, given that the content is changing completely. The top? The same line number as before? Neither seems satisfactory.

jonsterling commented 5 years ago

@cangiuli That's a good point! I'm ok with this behavior. I found it a little surprising, but it doesn't bother me.