Zulip Chat Archive

Stream: new members

Topic: VSCode

Paul van Wamelen (Feb 17 2020 at 16:45):

Is there some way to tell VSCode to insert 2 spaces instead of 4 when I hit tab?

Paul van Wamelen (Feb 17 2020 at 16:56):

Just noticed that if I start editing a brand new file, tab seems to equal 4 spaces, but if I edit an existing (2 space indented file), tab seems to generate 2 spaces. Is this a by file setting or is VSCode just being really smart?

Paul van Wamelen (Feb 17 2020 at 16:57):

Anyway, it kind of solves my "issue".

Chris Hughes (Feb 17 2020 at 16:59):

There's something called tab-size in the settings

Johan Commelin (Feb 17 2020 at 17:19):

Paul van Wamelen (Feb 17 2020 at 20:45):

Found my settings.json here (in case other windows users are wondering)
C:\Users\pvanwamelen\AppData\Roaming\Code\User
Thanks @Johan Commelin!

Paul van Wamelen (Feb 17 2020 at 20:47):

Also found the setting in the UI: Click on the gear near the lower left, then Settings. Type "tab size" in the search box. Thanks @Chris Hughes

Kevin Buzzard (Feb 17 2020 at 21:39):

You can access the settings direct from VS Code via File->Preferences->Settings

Patrick Lutz (May 17 2020 at 18:14):

Is there a keyboard shortcut in VS Code to pause and unpause Lean while writing a proof (or I guess in VS Code terminology maybe "freeze display" or "unfreeze display")? I find it annoying to use the mouse because it means the frame where I am writing the proof loses focus so I need to move the mouse around to start writing again. I tried looking at VS Code's reference list of keyboard shortcuts but couldn't find what I wanted.

Patrick Stevens (May 17 2020 at 18:15):

The action is "Lean: Info view: Toggle Updating"

Patrick Stevens (May 17 2020 at 18:16):

You can set your own keyboard shortcuts from the VS Code preferences

Patrick Lutz (May 17 2020 at 18:17):

Sorry if this is a dumb question, but how do I edit my preferences in VS Code?

Patrick Stevens (May 17 2020 at 18:17):

https://code.visualstudio.com/docs/getstarted/keybindings

Patrick Stevens (May 17 2020 at 18:17):

Depends on the operating system

Bryan Gin-ge Chen (May 17 2020 at 18:18):

Click the gear in the bottom left and you should see "keyboard shortcuts" in the menu. Then type in "toggle updating" and the Lean command should appear.

Patrick Lutz (May 17 2020 at 18:19):

Thanks! I actually tried looking for preferences in the menu under File but missed it for some reason

Mario Carneiro (May 17 2020 at 18:29):

VSCode has something much better than the "hunting through menus" experience of previous MS products like word and visual studio: Type ctrl-shift-P and then you can search for anything vscode knows how to do

Patrick Lutz (May 17 2020 at 18:29):

If for some reason I wanted to type ɛn when using Lean in VS Code, I would currently do something like type "\eps<space><backspace>n". Is there a way to avoid this? E.g. maybe a keyboard shortcut to automatically convert latex code like \eps into the symbol ɛ in the VS Code Lean editor?