syntax highlighting

Stream: general

[Kevin Buzzard]

William Stein says:

"Kevin - which of the modes listed here is closest to working for lean code?

https://codemirror.net/mode/index.html

I can modify an existing syntax highlighting mode to make it work properly..."

[Kevin Buzzard]

More details from someone else at cocalc:

[Kevin Buzzard]

"Regarding code editor syntax highlighting, I haven't found a good highlighting. Maybe we can create one for codemirror, though. Is there a simple language definition, where we for example can get a concise list of all keywords? I also checked what they are doing for that online live "lean" editor. This interface is based on the "monaco" editor [1]. They seem to have written their own plugins for it. CoCalc doesn't use Monco, but CodeMirror, though."

[Ian Riley]

I know that this is four years old, but I was hoping that we could revisit this topic. There are several applications that use CodeMirror for syntax highlighting. We already have syntax highlighting files for VS Code and NVIM. It should be fairly straightforward to configure a CodeMirror syntax highlighting file. It's essentially just a rewrite of the NVIM syntax highlighting configuration into JavaScript. Has this been revisited in the last four years?

[Eric Wieser]

A word of warning about codemirror from another topic:

Eric Wieser said:

Apparently its editor, CodeMirror, doesn't handle things that use two UTF-16 code units

So some lean files contain characters that CodeMirror doesn't support

[Ian Riley]

That's good to know. So my interest in CM is actually because of this https://github.com/deathau/cm-editor-syntax-highlight-obsidian I'd like to start putting Lean code into my Obsidian notes. I have an active PR atm to add lean support to the execute code plugin so that lean snippets can be executed in Obsidian MD but they don't have syntax highlighting without CM support.