Email Gateway (Nov 13 2022 at 20:22): 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: Apr 26 2024 at 01:06 UTC