Zulip Chat Archive

Stream: new members

Topic: VSCode


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

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

view this post on Zulip Paul van Wamelen (Feb 17 2020 at 16:57):

Anyway, it kind of solves my "issue".

view this post on Zulip Chris Hughes (Feb 17 2020 at 16:59):

There's something called tab-size in the settings

view this post on Zulip Johan Commelin (Feb 17 2020 at 17:19):

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

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

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

view this post on Zulip Kevin Buzzard (Feb 17 2020 at 21:39):

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

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

view this post on Zulip Patrick Stevens (May 17 2020 at 18:15):

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

view this post on Zulip Patrick Stevens (May 17 2020 at 18:16):

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

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

view this post on Zulip Patrick Stevens (May 17 2020 at 18:17):

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

view this post on Zulip Patrick Stevens (May 17 2020 at 18:17):

Depends on the operating system

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

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

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

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

view this post on Zulip Patrick Massot (May 17 2020 at 18:29):

Revolutionary! One day they will invent the command line.

view this post on Zulip Patrick Massot (May 17 2020 at 18:30):

TAB

view this post on Zulip Patrick Lutz (May 17 2020 at 18:30):

Thanks for the help

view this post on Zulip Mario Carneiro (May 17 2020 at 18:30):

this is why you should use fish shell

view this post on Zulip Patrick Lutz (May 17 2020 at 18:30):

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

view this post on Zulip Patrick Massot (May 17 2020 at 18:31):

This is a very recent phenomenon

view this post on Zulip Patrick Massot (May 17 2020 at 18:31):

Everybody used to be called Kevin

view this post on Zulip Patrick Lutz (May 17 2020 at 18:31):

This is the first time I've used zulip

view this post on Zulip Patrick Massot (May 17 2020 at 18:33):

Welcome!

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

view this post on Zulip Patrick Lutz (May 17 2020 at 18:34):

lol, thanks

view this post on Zulip 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: May 17 2021 at 21:12 UTC