Zulip Chat Archive

Stream: new members

Topic: Vs code interface questions


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Alex J. Best (Oct 15 2020 at 00:23):

same thing to unpause after

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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