Gergely Buday (Jun 20 2023 at 09:27): Gergely Buday (Jun 20 2023 at 09:27):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.
Fabian Huch (Jun 20 2023 at 09:37):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.
Gergely Buday (Jun 20 2023 at 09:46):Yes, approximations, but even a partial solution is better than nothing. And there are many people on Proof Assistants.
Gergely Buday (Jun 20 2023 at 09:50):By browser_info do you mean src/Pure/Thy/browser_info.scala?
Fabian Huch (Jun 20 2023 at 10:35):Yes.
Gergely Buday (Jun 20 2023 at 12:35):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: May 02 2024 at 04:18 UTC