rst preview vscode

Stream: general

[Gihan Marasingha]

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?

[Kevin Buzzard]

@Jeremy Avigad :point_up:

[Jeremy Avigad]

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]

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

[Gihan Marasingha]

And I hope you all get the correct result tomorrow.

[Gihan Marasingha]

@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]

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]

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

[Julian Berman]

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]

(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]

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]

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]

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

[Julian Berman]

ah that yeah sounds like an even better idea

[Alex Peattie]

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

image.png

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