Zulip Chat Archive

Stream: general

Topic: syntax highlighting

Kevin Buzzard (Jun 25 2018 at 16:42):

William Stein says:

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


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

Kevin Buzzard (Jun 25 2018 at 16:48):

More details from someone else at cocalc:

Kevin Buzzard (Jun 25 2018 at 16:48):

"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 (Dec 01 2022 at 16:42):

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 (Dec 01 2022 at 17:16):

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 (Dec 02 2022 at 04:08):

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.

Last updated: Aug 03 2023 at 10:10 UTC