## Stream: new members

### Topic: Vs code interface questions

#### Michael Beeson (Oct 15 2020 at 00:10):

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 (Oct 15 2020 at 00:21):

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 (Oct 15 2020 at 00:22):

1. 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 (Oct 15 2020 at 00:23):

same thing to unpause after

#### Alex J. Best (Oct 15 2020 at 00:24):

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 (Oct 15 2020 at 00:28):

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 (Oct 15 2020 at 00:37):

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 (Oct 15 2020 at 00:38):

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 (Oct 15 2020 at 00:39):

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

Last updated: May 16 2021 at 21:11 UTC