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):
- 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):
- 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
Last updated: May 16 2021 at 21:11 UTC