New Plugin for Obsidian

Stream: general

[Tomaz Mascarenhas]

Hi people,

I would like to share a plugin that I wrote for Obsidian, which provides syntax highlight for Lean codeblocks: https://github.com/tomaz1502/lean-syntax-highlight

It is already available in the "community plugins" section, so you can use by simply browsing and installing it with the plugin manager.

I would love to hear your feedback :) (also, please note that this is the very first javascript code I wrote) (yes, I like Lean to the point of learning a bit javascript because of it)

[Eric Wieser]

It might be worth publishing a standalone codemirror package for Lean too; in principle that would give us syntax highlighting in the github editor too, but in practice we can't have nice things when it comes to highlighters (GitHub doesn't support anything but first-party highlighters, and CodeMIrror doesn't accept new languages)

[Eric Wieser]

@Bryan Gin-ge Chen wrote a CodeMirror highlighter for Lean 3 at https://observablehq.com/@bryangingechen/hello-lean-prover#initCodeMirrorLeanMode, which might have some tricks you could copy

[Tomaz Mascarenhas]

Given their response in your comment, maybe we can get the nice things by sending a ticket to Github? But yeah, I will publish an npm package either way.

[Jireh Loreaux]

@Tomaz Gomes it seems the Obsidian plugin is broken. Do you happen to know of an easy fix?

I saw your open PR for Prism, which would solve this outright. Maybe we can get some more eyes :eyes: on that and get people to comment.

[Tomaz Mascarenhas]

Hm, I just updated Obsidian and did some quick tests and it seems working here. Could you share which steps you took?

[Tomaz Mascarenhas]

I agree, if the PR was merged then we would get for free highlight for Lean in Obsidian and in many other places that rely on Prism. Unfortunately it seems that the repository have not been maintained for a while :(

[Jireh Loreaux]

Hmmm... strange. It stopped working on one machine yesterday, and then today it wouldn't load on another machine either. But I just tested again and it seems to be working. Will post again if I can repro. Sorry for the noise.