Where is the code that does the html syntax highlighting for e.g. this theory file in the Archive of Formal Proofs?
There is another syntax highlighting engine on ProofCraft Blog using Pygments. As I see ZulipChat also uses Pygments.
I initiated a student project on adding Isabelle syntax highlighting to Highlight JS. Is there any other effort to do this? It could be used on the Proof Assistants Stack Exchange site.
Is highlight.js used anywhere prominent? There already is rouge, which is also ruby-based and used by github - I added Isabelle there a while ago.
The HTML highlighting on the AFP website on the other hand is generated by Isabelle (have a look at the browser_info module). This is the only proper way to get syntax highlighting as defining syntax is a user-space operation, so there is not static syntax for Isabelle. All these highlighters are mere (bad) approximations.
Yes, approximations, but even a partial solution is better than nothing. And there are many people on Proof Assistants.
By browser_info do you mean src/Pure/Thy/browser_info.scala
?
Yes.
If you want to follow the chances of getting a syntax highlighter for Isabelle onto the Proof Assistans Stack Exchange site, follow this question on Proof Assistants Meta.
Last updated: Jan 05 2025 at 08:21 UTC