Zulip Chat Archive

Stream: general

Topic: rst preview vscode


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

view this post on Zulip Kevin Buzzard (Nov 02 2020 at 17:24):

@Jeremy Avigad :point_up:

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

view this post on Zulip Gihan Marasingha (Nov 02 2020 at 17:33):

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

view this post on Zulip Gihan Marasingha (Nov 02 2020 at 17:34):

And I hope you all get the correct result tomorrow.

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

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

view this post on Zulip Julian Berman (Nov 02 2020 at 19:29):

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

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

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

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

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

view this post on Zulip Bryan Gin-ge Chen (Nov 02 2020 at 20:57):

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

view this post on Zulip Julian Berman (Nov 02 2020 at 22:42):

ah that yeah sounds like an even better idea

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

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


Last updated: May 06 2021 at 21:09 UTC