JP (Apr 15 2024 at 10:41): JP (Apr 15 2024 at 10:41):Hello! I am interested in creating websites similar to the one that I found at https://www.isa-afp.org/entries/CRDT.html. I was wondering if it is possible to customize the HTML output, for instance, to include only the body content without all the HTML headers and other elements. To ignore all the text expressions, to extract indexes of the types, terms, and theories present in the development, perhaps in a different format, idk, JSON, or something easier to manipulate. I'd like to integrate Isabelle's HTML output with my documentation site, which uses Markdown. So, I would really appreciate a beginner's guide on how to build the compiler and any helpful advice on this matter. The ideal would be Markdown support, as Agda has, i.e., something you could write markdown and only process the isabelle code blocks.
Thank you!
Fabian Huch (Apr 15 2024 at 10:54):Are you talking about the theory view within the AFP website or the website itself? And what are you trying to accomplish?
Fabian Huch (Apr 15 2024 at 10:54):If you want to build 'your own AFP-like thing' then all you need is the Isaelle HTML generation, otherwise you also need the AFP sitegen.
JP (Apr 15 2024 at 11:15):Hi Fabian, let me try again. The documentation tool I'm using uses markdown (mkdocs), and I'd like to show Isabelle's theories using my own layout. I have done that with Agda, using its literate markdown support, https://agda.readthedocs.io/en/v2.6.4.3/tools/literate-programming.html#literate-markdown-and-typst. It seems Isabelle does have that. And, I know one could use syntax highlighting support for Isabelle with some JS/pygments plugin, but again, that's not really what I want. I want isabelle code snippets to be clickable, as they were generated using the Isabelle HTML common procedure.
Fabian Huch (Apr 15 2024 at 11:21):I see. In this case you can use the Browser_Info module (src/Pure/Build/browser_info.scala) to do that from Isabelle/Scala: You can customize exactly what is generated.
You'll have to do this from an Isabelle context though, because that information is not known statically but only by running the theories. Its best to look into the manual how to create your custom Isabelle/Scala add-on component.
Last updated: May 06 2024 at 16:21 UTC