[isabelle-dev] Syntax highlighting for approx. 300 languages via Prism.js

Makarius makarius at sketis.net
Sun Nov 13 21:22:24 CET 2022


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


More information about the isabelle-dev mailing list