Zulip Chat Archive

Stream: general

Topic: vscode snippets

Johan Commelin (Feb 12 2019 at 13:11):

@Patrick Massot and others: is there some place where we gather useful VScode snippets?

Patrick Massot (Feb 12 2019 at 13:11):

No yet afaik

Johan Commelin (Feb 12 2019 at 13:11):

I couldn't find them online. Only some examples here on Zulip.

Johan Commelin (Feb 12 2019 at 13:11):

@Patrick Massot Would you mind putting yours in a gist, for starters?

Patrick Massot (Feb 12 2019 at 13:12):

I think having them inside the extension is controversial, but we could maintain a collection at mathlib

Johan Commelin (Feb 12 2019 at 13:12):

Sure, or in the extension repo, in a file that isn't shipped by default.

Johan Commelin (Feb 12 2019 at 13:13):

There could be a contrib folder in that repo.

Johan Commelin (Feb 12 2019 at 13:13):

But let's start with gists (-;

Patrick Massot (Feb 12 2019 at 13:13):

https://gist.github.com/PatrickMassot/27417fad299a48e690ab5609a99baa67

Patrick Massot (Feb 12 2019 at 13:17):

Speaking of the VScode extension, what happened to the Lean messages update icon?

Patrick Massot (Feb 12 2019 at 13:17):

@Gabriel Ebner

Gabriel Ebner (Feb 12 2019 at 13:19):

The Updating ⏸ icon in the top right? Is it broken?

Patrick Massot (Feb 12 2019 at 13:20):

update.png

Gabriel Ebner (Feb 12 2019 at 13:23):

vscode-updating.png :shrug:

Gabriel Ebner (Feb 12 2019 at 13:23):

Windows?

Patrick Massot (Feb 12 2019 at 13:23):

Are you talking to me in that last line? :angry_cat:

Gabriel Ebner (Feb 12 2019 at 13:23):

Yes.

Patrick Massot (Feb 12 2019 at 13:24):

Last windows I used was Windows 98. I'm not even sure you were born at that time

Gabriel Ebner (Feb 12 2019 at 13:26):

You had a few machines for students with windows (I think), that's why I asked. But now I'm even more at a loss..

Patrick Massot (Feb 12 2019 at 13:27):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/VScode.20extension/near/157785947

Patrick Massot (Feb 12 2019 at 13:27):

Bryan also had this issue

Gabriel Ebner (Feb 12 2019 at 13:28):

Oh, I'm still on 1.30 here. Thanks for the pointer!

Patrick Massot (Feb 12 2019 at 13:28):

If it's a VScode bug then at least my students won't see it in our computer labs with no VScode auto-update

Gabriel Ebner (Feb 12 2019 at 13:45):

The bug is already fixed in vscode master: https://github.com/Microsoft/vscode/issues/68033 We'll just have to wait for 1.31.1

Bryan Gin-ge Chen (Feb 13 2019 at 05:56):

1.31.1 just arrived and it looks like this is fixed!

Johan Commelin (Feb 13 2019 at 07:28):

Coming back to the original topic of this thread: I invite everyone who has useful VScode snippets to put them in a gist and post the url here.

Bryan Gin-ge Chen (Oct 26 2019 at 12:00):

Bumping this old thread to share something to make working with the "Infer type" hole command slightly easier. It's a snippet triggered by keybind rather than by auto-suggest. This will let you select a Lean expression and then hit "ctrl+'" to surround it with {! !}. You can then display the hole command menu by clicking on the light bulb icon that pops up or hitting your "Quick fix" keybind (cmd+. on mac).

To set this up, paste the following as an element of the array in your keybindings.json (you can get to it by hitting ctrl+shift+p (or cmd+shift+p on a mac) and typing "key j" and selecting "Open keyboard shortcuts (JSON)"):

    {
        "key": "ctrl+'",
        "command": "editor.action.insertSnippet",
        "when": "editorLangId == 'lean'",
        "args": {
            "snippet": "{!${TM_SELECTED_TEXT}!}"
        },
    }

Johan Commelin (Oct 26 2019 at 15:19):

@Bryan Gin-ge Chen Thanks, nice snippet!

Scott Morrison (Oct 27 2019 at 06:45):

Would this be unreasonable to put in .vscode/settings.json in the mathlib repository?

Miguel Raz Guzmán Macedo (Nov 12 2019 at 19:27):

beautiful snippets!
These reaaaally help beginners!

Last updated: Dec 20 2023 at 11:08 UTC