Stream: general

Topic: rst preview vscode

Gihan Marasingha (Nov 02 2020 at 17:15):

I've started making lecture notes for my 1st year undergrad course, initially using the template provided by Theorem Proving in Lean, but now using Mathematics in Lean. I'm writing the source in vscode with the reStructuredText extension. Initially, the extension's preview function worked fine, but after changing to the Mathematics in Lean template, the extension isn't rendering the maths, cross-references, etc.

Does anyone with experience of this know what to do? Or is there a better extension?

Jeremy Avigad (Nov 02 2020 at 17:32):

I am afraid I don't use the rst previewer. My workflow, when proofreading, is to open the html in a browser (you can find it in the build directory). I just build from the VS Code terminal and then press the reload button on the browser.

Gihan Marasingha (Nov 02 2020 at 17:33):

Thanks. That's what I've started doing now!

Gihan Marasingha (Nov 02 2020 at 17:34):

And I hope you all get the correct result tomorrow.

Gihan Marasingha (Nov 02 2020 at 18:03):

@Jeremy Avigad I have another related question. Is there a nice way to enter unicode characters when editing rst files in vscode? I usually end up just copying & pasting from Lean source.

Jeremy Avigad (Nov 02 2020 at 18:07):

That's exactly what I do. I always have a Lean scratch file open nearby. It's kind of annoying -- if anyone knows of a better way, I'd be happy to hear it.

Julian Berman (Nov 02 2020 at 19:29):

At least a way, if not the best way, would be loading them via snippets

Julian Berman (Nov 02 2020 at 19:30):

I haven't really had to write enough rst+lean to automatically do so myself, but yeah I have all the replacements in a ultisnips snippet file and can load them manually even when writing rst if I wanted to

Julian Berman (Nov 02 2020 at 19:30):

(you can do similar things in VSCode I think, it has its own snippet format but probably can be coerced into reading Ultisnips too)

Jeremy Avigad (Nov 02 2020 at 20:09):

Thanks for the suggestion. That may be worth a try. Just having the quantifiers, logical connectives, and some Greek letters would go a long way.

Bryan Gin-ge Chen (Nov 02 2020 at 20:57):

The Lean VSCode extension does allow turning on the unicode input for other file types, by setting lean.input.languages. I haven't tried this feature out so I'm not sure of the syntax.

Bryan Gin-ge Chen (Nov 02 2020 at 20:57):

It shows up in the list of Lean extension settings as "Lean > Input: Languages".

Julian Berman (Nov 02 2020 at 22:42):

ah that yeah sounds like an even better idea

Alex Peattie (Nov 03 2020 at 05:46):

Bryan Gin-ge Chen said:

The Lean VSCode extension does allow turning on the unicode input for other file types, by setting lean.input.languages. I haven't tried this feature out so I'm not sure of the syntax.

Yes I think this is the best approach :smile:. To expand on exactly how to do it, launch the Command Palette, then choose "Preferences: Open User Settings", search for "Lean > Input: Languages", click Add Item

Then put in the lowercase language identifier for the language you want to enable unicode input for. So if you're using this extension for rst, it'd be restructuredtext

Last updated: May 06 2021 at 21:09 UTC