Vs code interface questions

Stream: new members

[Michael Beeson]

Question 1: I would like to select a block and move that whole block left or right so many spaces. Is it possible?

Question 2: I would like the info view not to recalculate at every keystroke but only when I press Enter. Long ago I read that this is possible but I have no idea how to get it to happen. I like to compose long exact proofs a piece at a time and I need to see the current list of hypotheses while I do that.

[Alex J. Best]

1. Answering a slightly more general question: Press cmd-shift-p (on mac, probably ctrl-shift-p on windows?) and type what you want (in this case "indent") and you should see a line saying "indent line" with the hotkey next to it. On my machine it is "cmd+]" and then "cmd+[" to unindent.

[Alex J. Best]

2. Same thing cmd+shift+p and type toggle updating, and press enter to pause updating, there is no hotkey by default for this but you can set one

[Alex J. Best]

same thing to unpause after

[Alex J. Best]

to set a hotkey for something do "cmd+shift+p" type keyboard shortcuts and press enter, then type toggle updating to find that one setting and click that + next to it to set a keyboard shortcut

[Bryan Gin-ge Chen]

For 1. I usually select the text and then just hit tab or shift+tab to indent / de-indent by 2 spaces (the number of spaces in an indent is configurable.)

[Pedro Minicz]

For question 1: if you are a Vim user, there is a good plugin: VS Code Neovim. I am sure there is a good one for Emacs (but there is an Emacs mode for Lean, so that should be better).

[Pedro Minicz]

For question 2: I use ctrl+k to freeze the tactic display. It is a custom binding, so you can find one that fits you. It is very handy.

[Pedro Minicz]

To add a shortcut, install the Lean plugin and go to File > Preferences > Keyboard shortcuts and search for toggle updating.