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):

See also https://github.com/leanprover-community/mathlib/tree/master/.vscode

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?

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

Revolutionary! One day they will invent the command line.

Patrick Massot (May 17 2020 at 18:30):

TAB

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

Thanks for the help

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

this is why you should use fish shell

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

I'm a little disturbed at the percentage of Patricks in this chat

Patrick Massot (May 17 2020 at 18:31):

This is a very recent phenomenon

Patrick Massot (May 17 2020 at 18:31):

Everybody used to be called Kevin

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

This is the first time I've used zulip

Patrick Massot (May 17 2020 at 18:33):

Welcome!

Patrick Massot (May 17 2020 at 18:34):

It's dinner time, so I'll let another Patrick answer your questions (and you can still fall back on the legacy Kevin handler).

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

lol, thanks

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

Patrick Massot said:

Everybody used to be called Kevin

I must say, I preferred the days when I was called Kevin, but maybe that's just the usual nostalgia


Last updated: Dec 20 2023 at 11:08 UTC