FStarLang / fstar-mode.el

Emacs support for F*
Apache License 2.0
67 stars 17 forks source link

Pasting causes indentation #78

Closed kkohbrok closed 6 years ago

kkohbrok commented 6 years ago

Whenever I paste one or multiple lines while using fstar-mode (through the fstar-layer), that line (or lines) get indented. This is mostly deterministic, but in rare cases, indentation of copied code stays intact and in other cases, all indentation is preserved (which I would consider expected behaviour). I am not very familiar with the internal workings of emacs (and thus also spacemacs) and have thus not done much debugging. I'd be happy to investigate, though, if you have any pointers.

cpitclaudel commented 6 years ago

OK, reproduced. Thanks for the report; I'll look into it.

cpitclaudel commented 6 years ago

Can you try adding (add-to-list 'spacemacs-indent-sensitive-modes 'fstar-mode) to your .spacemacs somewhere? It should fix it.

cpitclaudel commented 6 years ago

That somewhere should be in dotspacemacs/user-config. Confirmed that it fixes it.

cpitclaudel commented 6 years ago

FTR, here's how I debugged this: I got a repro, then I pressed C-h k C-y to see what command pasting ran. Then I looked at the docs and saw that it was "advised" (meaning that extra code had been added to run around it), because it said :around advice: ‘ad-Advice-yank’. I clicked on that and saw this:

Around-advice ‘yank-indent’:
If current mode is not one of spacemacs-indent-sensitive-modes
 indent yanked text (with universal arg don’t indent).

Then I looked at the sources and found the original code and convinced myself that adding to indent-sensitive-modes was indeed the best solution.

Hope this makes the process more transparent :)

kkohbrok commented 6 years ago

It seems to fix it for pasting. As the behaviour has been somewhat non-deterministic in the past, I'll keep an eye on it in the next few days. However, it still indents whenever I move a line via the dotspacemacs-visual-line-move-text t. Its a really minor issue which I thought was related.

kkohbrok commented 6 years ago

Thanks a lot! I'll try to debug that "moving text" issue myself then :-)

cpitclaudel commented 6 years ago

Will look into that one too. Amusingly, reading through that code revealed a bug :) https://github.com/syl20bnr/spacemacs/pull/1485

cpitclaudel commented 6 years ago

I'll need your help to debug the second one — J and K seems to invoke Evil macros, and I have no idea how these work, unfortunately

cpitclaudel commented 6 years ago

https://github.com/syl20bnr/spacemacs/commit/ec35ede5b607b3f22332208e2e70806502999efd No idea why these macros do the things they do :)

kkohbrok commented 6 years ago

Sounds like some evil behaviour in spacemacs ;-) I can live with it. The copy-pasting behaviour was much more annoying.

cpitclaudel commented 6 years ago

Closing this, since it's a generic spacemacs issue. Feel free to reopen if you think there's something more I can do :)