Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Syntax highlighting for approx. 300 langua...

view this post on Zulip Email Gateway (Nov 13 2022 at 20:22):

From: Makarius <>
We have this bulky bundle of VSCodium/Electron/Node.js already, so the obvious
question is how to re-use that for other means than running Isabelle/VSCode.

I have recently encountered the old-school LaTeX syntax highlighting (e.g. in AFP), and wondered if the
Node.js/JavaScript world has a better alternative to offer.

The result of some web search is Prism.js, see also:


Isabelle/2615cf68f6f4 already supports Prismjs both in Isabelle/ML and
Isabelle/Scala. Here are some examples:

declare [[ML_print_depth = 2000]]
ML ‹Prismjs.languages () |> `length›
ML ‹Prismjs.tokenize {language = "scala", text =
ML ‹Prismjs.tokenize {language = "java", text =
ML ‹Prismjs.tokenize {language = "ada", text =
ML ‹Prismjs.tokenize {language = "bash", text =
ML ‹Prismjs.tokenize {language = "javascript", text =
ML ‹Prismjs.tokenize {language = "css", text =

To make proper use of it in PIDE markup or LaTeX documents, we need an
additional concept to replace the CSS rendering of the original product. It
should be sufficient to replace its token types by well-known PIDE markup
elements, but it needs some systematic management.


isabelle-dev mailing list

Last updated: Mar 04 2024 at 10:08 UTC