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 <makarius@sketis.net>
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
https://ctan.org/pkg/listings (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:

- https://prismjs.com
- https://www.npmjs.com/package/prismjs

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 = File.read
🗏‹~~/src/Pure/Tools/prismjs.scala›}›
ML ‹Prismjs.tokenize {language = "java", text = File.read
🗏‹~~/src/Tools/Setup/src/Environment.java›}›
ML ‹Prismjs.tokenize {language = "ada", text = File.read
🗏‹~~/src/HOL/SPARK/Manual/document/complex_types.ads›}›
ML ‹Prismjs.tokenize {language = "bash", text = File.read
🗏‹~~/lib/Tools/version›}›
ML ‹Prismjs.tokenize {language = "javascript", text = File.read
🗏‹$ISABELLE_PRISMJS_HOME/prism.js›}›
ML ‹Prismjs.tokenize {language = "css", text = File.read
🗏‹$ISABELLE_PRISMJS_HOME/themes/prism.css›}›

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.

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Last updated: Mar 04 2024 at 10:08 UTC